Integrating Gandalf and HOL

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.

• Type: Conference
• Year: 1999
• Where: TPHOL
• Authors: Joe Hurd
• Keywords: Automated Reasoning, First-order Resolution Theorem-prover, Gandalf, GANDALF TAC, TPHOL 1999