Isabelle Isabelle 是一个基于高阶逻辑higherorder logic的通用交互式定理证明器它是一个 LCFLogic for Computable Functions风格的证明辅助工具使用 Standard ML 语言实现它拥有一个极小化的逻辑核心这意味着使用它的证明和形式化验证具有较强的的可信度 Isabelle 是通用的它提供了一套元逻辑相当于一个较弱版本的类型论可用于编码诸多对象逻辑如一阶逻辑高阶逻辑或ZF集合论最常被用到的对象逻辑是 IsabelleHOL而其对集合论的形式化工作则使用了 IsabelleZFIsabelle 的主要证明手段利用了高阶版本的归结原理resolution基于高阶的合一unification 尽管 Isabelle 主要采取交互式的证明方式它同时亦提供了若干高效的自动化推理工具例如项重写引擎tableaux 证明器以及各种判定过程藉由 sledgehammer 界面它还可以调用外部的 SMT 求解器包括 CVC和其他归结式定理证明器包括 E 和 SPASS Isabelle 被用于形式化数学和计算机科学中的许多定理诸如哥德尔完备性定理哥德尔关于选择公理一致性的证明素数定理各种安全协议的正确性程序语言语义的特性这些定理形式化工作的维护通过形式化证明存档Archive of Formal Proofs进行截至  年它已包含逾  个条目两百万行证明 Isabelle 定理证明器是开源软件其源码在 BSD license 下授权发布 Isabelle由其作者 Lawrence Paulson 命名这名字取自于法国计算机科学家 Gérard Huet英语Gérard Huet 的女儿