Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

13

TPHOL
1999
IEEE

favoriteEmaildiscussreport

108views Automated Reasoning» more TPHOL 1999»

Integrating Gandalf and HOL

13 years 9 months ago

Integrating Gandalf and HOL

Download www.cl.cam.ac.uk

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.

Joe Hurd

Real-time Traffic

Automated Reasoning | First-order Resolution Theorem-prover | Gandalf | GANDALF TAC | TPHOL 1999 |

claim paper

Related Content

» Importing HOL into IsabelleHOL

» Hybrid verification integrating HOL theorem proving with MDG model checking

» An Integration of HOL and ACL2

» On the Formalization of the Lebesgue Integration Theory in HOL

» Formal hardware verification by integrating HOL and MDG

» Providing Automated Verification in HOL Using MDGs

» Delay characteristics in discretetime GIG1 queues with nonpreemptive priority queueing dis...

» The Village Telephone System A Case Study in Formal Software Engineering

» Verifying a Compiler for Java Threads

Post Info
More Details (n/a)

Added	04 Aug 2010
Updated	04 Aug 2010
Type	Conference
Year	1999
Where	TPHOL
Authors	Joe Hurd

Comments (0)