Isabelle

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 个条目，两百万行证明。
Isabelle 定理证明器是开源软件，其源码在 BSD license 下授权发布。
“Isabelle”由其作者 Lawrence Paulson 命名；这名字取自于法国计算机科学家 Gérard Huet 的女儿。

== 示例 ==
Isabelle 支持两种不同风格的的证明书写方式：过程式和声明式。
过程式风格的证明主要由一系列证明策略（tactics）或过程的依次运用组成；它能够较好地反映数学家思考证明的过程，但通常较难阅读，因为它无法直接体现每步推演的结果。
声明式风格的证明（由 Isabelle 内置的证明语言 Isar 支持）则与之相反，它以直接的方式描述了每一步确切的数学推演，因此较容易被阅读和人工检查。
在较新版本的 Isabelle 中，过程式风格的证明已不建议再使用。形式化证明存档（Archive of Formal Proofs）亦推荐使用声明式风格来书写证明。
例如，下面是一个声明式风格的“2的算术平方根是无理数”的证明：

theorem sqrt2_not_rational:
"sqrt (real 2) ∉ ℚ"
proof
let ?x = "sqrt (real 2)"
assume "?x ∈ ℚ"
then obtain…