Substitution Tree Indexing

摘要: Sophisticated maintenance and retrieval of first-order predicate calculus terms is a major key to efficient automated reasoning. We present new indexing technique, which accelerates the speed basic operations such as finding complementary literals in resolution theorem proving or critical pairs during completion. Subsumption reduction are also supported. Moreover, technique not only provides but idem-potent substitutions. Substitution trees achieve maximal search paired with minimal memory requirements various experiments outperform traditional techniques path indexing, discrimination tree abstraction by combining their advantages adding some features.