TL;DR
Isabelle is a versatile, generic theorem prover supporting multiple formal theories, with a rich history and various logic representations, facilitating interactive reasoning across different logical systems.
Contribution
This paper provides a comprehensive overview of Isabelle's design, history, logic representations, and its role as a flexible platform for formal reasoning.
Findings
Supports multiple formal theories including type theory and set theory
Offers a detailed history and comparison with other logical frameworks
Includes descriptions of various Isabelle object-logics
Abstract
Isabelle is a generic theorem prover, designed for interactive reasoning in a variety of formal theories. At present it provides useful proof procedures for Constructive Type Theory, various first-order logics, Zermelo-Fraenkel set theory, and higher-order logic. This survey of Isabelle serves as an introduction to the literature. It explains why generic theorem proving is beneficial. It gives a thorough history of Isabelle, beginning with its origins in the LCF system. It presents an account of how logics are represented, illustrated using classical logic. The approach is compared with the Edinburgh Logical Framework. Several of the Isabelle object-logics are presented.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.