Computer Laboratory

Technical reports

Experience with Isabelle
A generic theorem prover

Lawrence C. Paulson

August 1988, 20 pages

Abstract

The theorem prover Isabelle is described briefly and informally. Its historical development is traced from Edinburgh LCF to the present day. The main issues are unification, quantifiers, and the representation of inference rules. The Edinburgh Logical Framework is also described, for a comparison with Isabelle. An appendix presents several Isabelle logics, including set theory and Constructive Type Theory, with examples of theorems.

Full text

PDF (0.2 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-143,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Experience with Isabelle : A generic theorem prover}},
  year = 	 1988,
  month = 	 aug,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-143.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-143}
}