Technical reports
Integrating Gandalf and HOL
March 1999, 11 pages
DOI: 10.48456/tr-461
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.
Full text
PDF (0.2 MB)
BibTeX record
@TechReport{UCAM-CL-TR-461, author = {Hurd, Joe}, title = {{Integrating Gandalf and HOL}}, year = 1999, month = mar, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-461.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-461}, number = {UCAM-CL-TR-461} }