Repository logo
 

ISABELLE - THE NEXT 700 THEOREM PROVERS

Accepted version
Peer-reviewed

Type

Article

Change log

Authors

PAULSON, LC 

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.

Description

Keywords

cs.LO, cs.LO, F.3.1; F.4.1

Journal Title

LECT NOTES COMPUT SC

Conference Name

Journal ISSN

0302-9743

Volume Title

310

Publisher

Publisher DOI

Publisher URL