The foundation of a generic theorem prover
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Paulson, LC
Abstract
Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in which the object-logics are formalized. Isabelle is now based on higher-order logic -- a precise and well-understood foundation. Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment. Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet's higher-order unification procedure.
Description
Keywords
cs.LO, cs.LO, F.3.1; F.4.1
Journal Title
Journal of Automated Reasoning
Conference Name
Journal ISSN
0168-7433
1573-0670
1573-0670
Volume Title
5
Publisher
Springer Science and Business Media LLC