Technical reports

# The foundation of a generic theorem prover

**Lawrence C Paulson**

March 1988, 44 pages

This paper is a revised version of UCAM-CL-TR-113.

## 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 = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf}, institution = {University of Cambridge, Computer Laboratory}, number = {UCAM-CL-TR-130} }