Sciweavers

59
Voted
TPHOL
1999
IEEE
15 years 1 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