Isabelle: The Next 700 Theorem Provers
By Lawrence Charles Paulson. arXiv.org, 2000
424 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/8f4c5327caee60e7cb1e22b903cc325875b3ca6a
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- M. Wenzel
- Tobias Nipkow
- Lawrence Charles Paulson
- Xavier Leroy
- Christian Szegedy
- Sean Welleck
- Rahul Saha
- Markus Norman Rabe
In Computational Theory and Mathematics
- M. Wenzel
- Tobias Nipkow
- Lawrence Charles Paulson
- Christian Szegedy
- Sean Welleck
- Rahul Saha
- Markus Norman Rabe
Citations in the corpus
- The Isabelle Framework (2008, background): “The Isabelle/Pure meta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics following the general idea of natural deduction [32, 33].”