Department of Computer Science and Technology

Technical reports

Integrating Gandalf and HOL

Joe Hurd

March 1999, 11 pages

DOI: 10.48456/tr-461


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

  author =	 {Hurd, Joe},
  title = 	 {{Integrating Gandalf and HOL}},
  year = 	 1999,
  month = 	 mar,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-461},
  number = 	 {UCAM-CL-TR-461}