Computer Laboratory

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

PDF (0.2 MB)
DVI (0.1 MB)

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}
}