Abstract
Gaining efficiency in completion-based theorem proving requires improvements on three levels: fast inference step execution, careful aggregation into an inference machine, and sophisticated control strategies, all that combined with space saving representation of derived facts. We introduce the new Waldmeister prover which shows an increase in overall system performance of more than one order of magnitude as compared with standard techniques.
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus and J. Denzinger. Distributing equational theorem proving. In Proc. 5th RTA, vol. 690 of LNCS, 1993.
A. Buch and Th. Hillenbrand. Waldmeister: Development of a high performance completion-based theorem prover. SEKI-Report 96-01, Universität Kaiserslautern, 1996.
J. Christian. Past Knuth-Bendix completion: A summary. In Proc. 3rd RTA, vol. 355 of LNCS, 1989.
P. Graf. Term Indexing, vol. 1053 of LNAI. Springer Verlag, 1995.
J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. 14th ICALP, vol. 267 of LNCS, 1987.
D.E. Knuth and P.B. Bendix. Simple word problems in universal algebra. Computational Problems in Abstract Algebra, 1970.
E. Lusk and R.A. Overbeek. Reasoning about equality. JAR, 2, 1985.
E. Lusk and L. Wos. Benchmark problems in which equality plays the major role. In Proc. 11th CADE, vol. 607 of LNCS, 1992.
W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. JAR, 8(3), 1992.
C.C. Sims. The Knuth-Bendix procedure for strings as a substitute for coset enumeration. JSR, 12, 1991.
A. Tarski. Logic, Semantics, Metamathematics. Oxford Univ. Press, 1956.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hillenbrand, T., Buch, A., Fettig, R. (1996). On gaining efficiency in completion-based theorem proving. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_74
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_74
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive