Abstract
Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and computationally intensive domain-specific proof procedures. The generality of tactic provers has a performance penalty; the speed of proof search lags far behind special-purpose provers. We present a new modular proving architecture that significantly increases the speed of the core logic engine. Our speedup is due to efficient data structures and modularity, which allows parts of the prover to be customized on a domain-specific basis. Our architecture is used in the MetaPRL logical framework, with speedups of more than two orders of magnitude over traditional tactic-based proof search.
Support for this research was provided by DARPA grants F30602-95-1-0047 and F30602-98-2-0198
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Peter Aczel. The type theoretic interpretation of constructive set theory: Inductive definition. In Logic, Methodology and Philosophy of Science VII, pages 17–49. Elsevier Science Publishers, 1986.
Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The semantics of reflected proof. In Proceedings of the Fifth Symposium on Logic in Computer Science, pages 95–197. IEEE, June 1990.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard-Mohring, Amokrane Saïbi, and Benjamin Werner. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, CNRS and ENS Lyon, 1996.
David A. Basin and M. Kaufmann. The Boyer-Moore prover and Nuprl: An experimental comparison. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 89–119. Cambridge University Press, 1991.
J. L. Bates. A Logic for Correct Program Development. PhD thesis, Cornell University, 1979.
R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979.
Robert L. Constable, T. Knoblock, and J.L. Bates. Writing programs that construct proofs. J. Automated Reasoning, 1(3):285–326, 1984.
Thierry Coquand, Bengt Nordström, Jan M. Smith, and Björn von Sydow. Type Theory and Programming. EATCS, February 1994. bulletin no 52.
Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A Tutorial Introduction to PVS. In WIFT’ 95: Workshop on Industrial-Strength Formal Specification Techniques, April 1995. http://www.csl.sri.com/sri-csl-fm.html.
R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. In The Journal of Symbolic Logic, pages Vol. 57, Number 3, September 1992.
R.L. Constable et.al. Implementing Mathematics in the NuPRL Proof Development System. Prentice-Hall, 1986.
M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, 1993.
John Harrison. HOL Light: A tutorial introduction. In Formal Methods in Computer-Aided Design (FMCAD’96), pages 265–269. Springer LNCS 1166, 1996.
Jason Hickey. Fault-tolerant distributed theorem proving. In Harald Ganzinger, editor, Automated Deduction — CADE-16, 16th International Conference on Automated Deduction, LNAI 1632, pages 227–231, Trento, Italy, July 7–10, 1999. Springer-Verlag.
Jason J. Hickey. Nuprl-Light: An implementation framework for higher-order logics. In 14th International Conference on Automated Deduction. Springer, 1997.
Douglas J. Howe. A type annotation scheme for Nuprl. In Theorem Proving in Higher-Order Logics. Springer, 1998.
Matt Kaufmann and J. Moore. An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering, 23(4):203–213, April 1997.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer LNCS 828, 1994.
Pierre Weis and Xavier Leroy. Le langage Caml. Dunod, Paris, 2nd edition, 1999. In French.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hickey, J., Nogin, A. (2000). Fast Tactic-Based Theorem Proving. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_16
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive