Isabelle: The Next 700 Theorem Provers
Isabelle: The Next 700 Theorem Provers
复制标题
DOI：
10.17863/cam.23640
复制
发表时间：
2000-10
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson
Isabelle是一个通用的定理证明器，设计用于各种形式理论的交互式推理。目前，它为构造型理论、各种一阶逻辑、Zermelo-Fraenkel集合论和高阶逻辑提供了有用的证明过程。这一调查伊莎贝尔作为一个介绍文学。它解释了为什么一般定理证明是有益的。它提供了一个彻底的历史伊莎贝尔，从它的起源在LCF系统。它提出了一个帐户的逻辑是如何表示，说明使用经典逻辑。该方法与爱丁堡逻辑框架进行了比较。几个伊莎贝尔对象逻辑。
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.