Abstract
Sophisticated maintenance and retrieval of first-order predicate calculus terms is a major key to efficient automated reasoning. We present a new indexing technique, which accelerates the speed of the basic retrieval operations such as finding complementary literals in resolution theorem proving or finding critical pairs during completion. Subsumption and reduction are also supported. Moreover, the new technique not only provides maintenance and efficient retrieval of terms but also of idem-potent substitutions. Substitution trees achieve maximal search speed paired with minimal memory requirements in various experiments and outperform traditional techniques such as path indexing, discrimination tree indexing, and abstraction trees by combining their advantages and adding some new features.
This work was supported by the German Science Foundation (DFG).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
L. Bachmair, T. Chen, and I.V. Ramakrishnan. Associative-commutative discrimination nets. In Proceedings TAPSOFT '93, LNCS 668, pages 61–74. Springer Verlag, 1993.
R. Butler and R. Overbeek. Formula databases for high-performance resolution/paramodulation systems. Journal of Automated Reasoning, 12:139–156, 1994.
J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95–113, February 1993.
P. Graf. Extended path-indexing. In 12th Conference on Automated Deduction, pages 514–528. Springer LNAI 814, 1994.
P. Graf. Substitution tree indexing. Technical Report MPI-I-94-251, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1994. Full version of this paper.
D. Knuth and P. Bendix. Simple Word Problems in Universal Algebras. Computational Problems in Abstract Algebras. Ed. J. Leech, Pergamon Press, 1970.
E. Lusk and R. Overbeek. Data structures and control architectures for the implementation of theorem proving programs. In 5th International Conference on Automated Deduction, pages 232–249. Springer Verlag, 1980.
W. McCune. Otter 2.0. In 10th International Conference on Automated Deduction, pages 663–664. Springer Verlag, 1990.
W. McCune. Experiments with discrimination-tree indexing and path-indexing for term retrieval. Journal of Automated Reasoning, 9(2):147–167, October 1992.
H.J. Ohlbach. Abstraction tree indexing for terms. In Proceedings of the 9th European Conference on Artificial Intelligence, pages 479–484. Pitman Publishing, London, August 1990.
J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.
M. Stickel. The path-indexing method for indexing terms. Technical Note 473, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graf, P. (1995). Substitution tree indexing. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_52
Download citation
DOI: https://doi.org/10.1007/3-540-59200-8_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59200-6
Online ISBN: 978-3-540-49223-8
eBook Packages: Springer Book Archive