Sciweavers

TPHOL
1999
IEEE
13 years 9 months ago
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 ...
Joe Hurd