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.
Cite
CITATION STYLE
Hurd, J. (1999). Integrating gandalf and hol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1690, pp. 311–321). Springer Verlag. https://doi.org/10.1007/3-540-48256-3_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
