Abstract
Gandalf is a first-order resolution theorem-prover, optimized for speed and specializing in manipulations of large clauses. In this paper I describe GANDALF TAC, a HOL tactic that proves goals by calling Gandalf and mirroring the resulting proofs in HOL. This call can occur over a network, and a Gandalf server may be set up servicing multiple HOL clients. In addition, the translation of the Gandalf proof into HOL fits in with the LCF model and guarantees logical consistency.
Supported by an EPSRC studentship
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.
Similar content being viewed by others
References
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, and Peter H. Schmitt. Integration of automated and interactive theorem proving. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications, volume II, chapter 4, pages 97–116. Kluwer, 1998.
H. Busch. First-order automation for higher-order-logic theorem proving. In Higher Order Logic Theorem Proving and Its Applications, volume Lecture Notes in Computer Science volume 859. Springer-Verlag, 1994.
M. J. C. Gordon and T. F. Melham. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993.
J. Harrison. Optimizing proof search in model elimination. In M. A. McRobbie and J. K. Slaney, editors, 13th International Conference on Automated Deduction, volume 1104 of Lecture Notes in Computer Science, pages 313–327, New Brunswick, NJ, 1996. Springer-Verlag.
J. Harrison. The HOL-Light Manual (1.0), May 1998. Available from http://www.cl.cam.ac.uk/users/jrh/hol-light/.
R. Kumar, Th. Kropf, and Schneider K. Integrating a first-order automatic prover in the hol environment. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications (HOL91), pages 170–176, Davis, California, August 1991. IEEE Computer Society Press.
K. Slind. HOL98 Draft User’s Manual, Athabasca Release, Version 2, January 1999. Available from http://www.cl.cam.ac.uk/users/kxs/.
T. Tammet. A resolution theorem prover for intuitionistic logic. In Cade 13, volume Lecture Notes in Computer Science volume 1104. Springer Verlag, 1996.
T. Tammet. Gandalf version c-1.0c Reference Manual, October 1997. Available from http://www.cs.chalmers.se/~tammet/.
T. Tammet. Towards efficient subsumption. In Automated Deduction: Cade 15, volume Lecture Notes in Artificial Intelligence volume 1421. Springer, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hurd, J. (1999). Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_21
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive