Technical reports
Experience with Isabelle
A generic theorem prover
August 1988, 20 pages
DOI: 10.48456/tr-143
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
BibTeX record
@TechReport{UCAM-CL-TR-143,
author = {Paulson, Lawrence C.},
title = {{Experience with Isabelle : A generic theorem prover}},
year = 1988,
month = aug,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-143.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-143},
number = {UCAM-CL-TR-143}
}