Isabelle

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

Isabelle

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

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]

示例

Isabelle 支持两种不同风格的的证明书写方式：过程式和声明式。 过程式风格的证明主要由一系列证明策略（tactics）或过程的依次运用组成；它能够较好地反映数学家思考证明的过程，但通常较难阅读，因为它无法直接体现每步推演的结果。 声明式风格的证明（由 Isabelle 内置的证明语言 Isar 支持）则与之相反，它以直接的方式描述了每一步确切的数学推演，因此较容易被阅读和人工检查。

在较新版本的 Isabelle 中，过程式风格的证明已不建议再使用。形式化证明存档（Archive of Formal Proofs）亦推荐使用声明式风格来书写证明。^[4]

例如，下面是一个声明式风格的“2的算术平方根是无理数”的证明：

theorem sqrt2_not_rational:
  "sqrt (real 2) ∉ ℚ"
proof
  let ?x = "sqrt (real 2)"
  assume "?x ∈ ℚ"
  then obtain m n :: nat where
    sqrt_rat: "¦?x¦ = real m / real n" and lowest_terms: "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  hence "real (m^2) = ?x^2 * real (n^2)" by (auto simp add: power2_eq_square)
  hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce
  hence "2 dvd m^2" by simp
  hence "2 dvd m" by simp
  have "2 dvd n" proof -
    from ‹2 dvd m› obtain k where "m = 2 * k" ..
    with eq have "2 * n^2 = 2^2 * k^2" by simp
    hence "2 dvd n^2" by simp
    thus "2 dvd n" by simp
  qed
  with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest)
  with lowest_terms have "2 dvd 1" by simp
  thus False using odd_one by blast
qed

应用

除数学证明以外，Isabelle 亦被广泛应用于计算机软件及硬件的形式化验证：

• 2009年，澳大利亚 NICTA 的 L4 团队开发了史上首个功能正确性得以形式化验证的通用操作系统内核：seL4 微内核。其证明使用 Isabelle/HOL 构建，包含了 200000 行证明脚本，用以验证 7500 行 C 代码。该形式化验证涵盖了代码、设计与实现，其主定理指出：该内核的 C 代码正确地实现了其形式化设计规范。
• 程序语言 Lightweight Java 类型安全的形式化证明使用了 Isabelle。^[5]

Isabelle 的网站上有一个使用 Isabelle 的研究项目列表^[6]。

参考文献

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）.
4. Archive of Formal Proofs. [2020-02-11]. （原始内容存档于2020-12-19）.
5. afp.sourceforge.net. [2020-02-11]. （原始内容存档于2016-03-19）.
6. 使用 Isabelle 的研究项目列表 （页面存档备份，存于互联网档案馆）

拓展阅读

• Lawrence C. Paulson. "The foundation of a generic theorem prover". Journal of Automated Reasoning, Volume 5, Issue 3 (September 1989), pages: 363–397, ISSN 0168-7433.
• Lawrence C. Paulson: The Isabelle Reference Manual.
• M. A. Ozols, K. A. Eastaughffe, and A. Cant. "DOVE: Design Oriented Verification and Evaluation". Proceedings of AMAST 97, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
• Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL – A Proof Assistant for Higher-Order Logic.

外部链接

• Isabelle 的官方网站 （页面存档备份，存于互联网档案馆）
• 形式化证明存档（The Archive of Formal Proofs） （页面存档备份，存于互联网档案馆）
• IsarMathLib （页面存档备份，存于互联网档案馆）