Isabelle
 運行在 macOS 之上的 Isabelle/jEdit | |
| 原作者 | Lawrence Paulson |
|---|---|
| 開發者 | 劍橋大學、慕尼黑工業大學 |
| 首次發布 | 1986[1] |
| 當前版本 | 2022 |
| 編程語言 | Standard ML、Scala |
| 操作系統 | Linux、Windows、macOS |
| 類型 | 數學 |
| 許可協議 | BSD license |
| 網站 | 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 個條目，兩百萬行證明。[2]
Isabelle 定理證明器是開源軟件，其源碼在 BSD license 下授權發布。
「Isabelle」由其作者 Lawrence Paulson 命名；這名字取自於法國計算機科學家 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]。
參考文獻
- ^ 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.
- ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. Archive of Formal Proofs. [22 October 2019]. （原始內容存檔於2020-12-19）.
- ^ Gordon, Mike. 1.2 History. Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). 1994-11-16 [2016-04-28]. （原始內容存檔於2017-03-05）.
- ^ Archive of Formal Proofs. [2020-02-11]. （原始內容存檔於2020-12-19）.
- ^ afp.sourceforge.net. [2020-02-11]. （原始內容存檔於2016-03-19）.
- ^ 使用 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.