Technical reports

Isabelle’s object-logics

Lawrence C. Paulson

February 1993, 161 pages

DOI: 10.48456/tr-286

Abstract

Several logics come with Isabelle. Many of them are sufficiently developed to serve as comfortable reasoning environments. They are also good starting points for defining new logics. Each logic is distributed with sample proofs, some of which are presented in the paper. The logics described include first-order logic, Zermelo-Fraenkel set theory, higher-order logic, constructive type theory, and the classical sequent calculus LK. A final chapter explains the fine points of defining logics in Isabelle.

Full text

DVI (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-286,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Isabelle's object-logics}},
  year = 	 1993,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-286.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-286},
  number = 	 {UCAM-CL-TR-286}
}