Technical reports
The foundation of a generic theorem prover
March 1988, 44 pages
This paper is a revised version of UCAM-CL-TR-113.
DOI: 10.48456/tr-130
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.
Full text
BibTeX record
@TechReport{UCAM-CL-TR-130,
author = {Paulson, Lawrence C},
title = {{The foundation of a generic theorem prover}},
year = 1988,
month = mar,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-130},
number = {UCAM-CL-TR-130}
}