Isabelle

Isabelle

运行在 macOS 之上的 Isabelle/jEdit
原作者	Lawrence Paulson（英语：Lawrence Paulson）
開發者	剑桥大学、慕尼黑工业大学
首次发布	1986[1]
当前版本	2022
编程语言	Standard ML、Scala
操作系统	Linux、Windows、macOS
类型	数学
许可协议	BSD license
网站	isabelle.in.tum.de

Isabelle 是一个基于高阶逻辑（higher-order logic）的通用交互式定理证明器。它是一个 LCF（Logic for Computable Functions）风格的证明辅助工具，使用 Standard ML 语言实现。它拥有一个极小化的逻辑核心；这意味着使用它的证明和形式化验证具有较强的的可信度。

Isabelle 是通用的：它提供了一套元逻辑（相当于一个较弱版本的类型论），可用于编码诸多对象逻辑，如一阶逻辑、高阶逻辑、或ZF集合论。最常被用到的对象逻辑是 Isabelle/HOL；而其对集合论的形式化工作则使用了 Isabelle/ZF。Isabelle 的主要证明手段利用了高阶版本的归结原理（resolution），基于高阶的合一（unification）。

尽管 Isabelle 主要采取交互式的证明方式，它同时亦提供了若干高效的自动化推理工具，例如项重写引擎、tableaux 证明器、以及各种判定过程。藉由 sledgehammer 界面，它还可以调用外部的 SMT 求解器（包括 CVC4）和其他归结式定理证明器（包括 E 和 SPASS）。

Isabelle 被用于形式化数学和计算机科学中的许多定理，诸如哥德尔完备性定理、哥德尔关于选择公理一致性的证明、素数定理、各种安全协议的正确性、程序语言语义的特性。这些定理形式化工作的维护通过形式化证明存档（Archive of Formal Proofs）进行；截至 2019 年它已包含逾 500 个条目，两百万行证明。^[2]

Isabelle 定理证明器是开源软件，其源码在 BSD license 下授权发布。

“Isabelle”由其作者 Lawrence Paulson 命名；这名字取自于法国计算机科学家 Gérard Huet（英语：Gérard Huet） 的女儿。^[3]

1. ^ Paulson, L. C. Natural deduction as higher-order resolution. The Journal of Logic Programming. 1986, 3 (3): 237. arXiv:cs/9301104 . doi:10.1016/0743-1066(86)90015-4. 
2. ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. Archive of Formal Proofs. [22 October 2019]. （原始内容存档于2020-12-19）. 
3. ^ Gordon, Mike. 1.2 History. Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). 1994-11-16 [2016-04-28]. （原始内容存档于2017-03-05）.