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 亦被廣泛應用於計算機軟件及硬件的形式化驗證:
Isabelle 的網站上有一個使用 Isabelle 的研究項目列表[6]。
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.