Paper Info
Title
An LCF-Style Interface between HOL and First-Order Logic
Abstract
Performing interactive proof in the HOL theorem prover1 [3] involves reducing goals to simpler subgoals. It turns out that many of these subgoals can be efficiently ‘finished off’ by an automatic first-order prover. To fill this niche, Harrison implemented a version of the MESON procedure [4] with the ability to translate proofs to higher-order logic. This was integrated as a HOL tactic in 1996, and has since become a standard workhorse of interactive proof. Today, building all the theories in the most recent distribution of HOL relies on MESON to prove 1726 subgoals.
Year
DOI
Venue
2002
10.1007/3-540-45620-1_10
CADE
Keywords
Field
DocType
first-order logic,lcf-style interface,higher order logic,first order logic,first order
HOL,Discrete mathematics,Computer science,Automated theorem proving,Algorithm,First-order logic,Mathematical proof,Metalanguage,Gas meter prover
Conference
ISBN
Citations 
PageRank 
3-540-43931-5
20
1.21
References 
Authors
5
1
Name
Order
Citations
PageRank
Joe Hurd1898.92