Technical reports
Isabelle’s object-logics
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} }