Technical reports

Integrating Gandalf and HOL

Joe Hurd

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}
}