Isabelle: The Next 700 Theorem Provers

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.

Cited by in corpus (8)

• QED at Large: A Survey of Engineering of Formally Verified Software
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
• Permissive-Nominal Logic (journal version)
• A modular construction of type theories
• Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie?
• A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras
• Interpolation and Quantifiers in Ortholattices
• Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice