text: Isabelle 是一個基於高階邏輯風格的證明輔助工具，使用 Standard ML 語言實現。它擁有一個極小化的邏輯核心；這意味著使用它的證明和形式化驗證具有較強的的可信度。Isabelle 是通用的：它提供了一套元邏輯。儘管 Isabelle 主要採取互動式的證明方式，它同時亦提供了若干高效的自動化推理工具，例如項重寫引擎、tableaux 證明器、以及各種判定過程。藉由 "sledgehammer" 介面，它還可以呼叫外部的 SMT 求解器。Isabelle 被用於形式化數學和計算機科學中的許多定理，諸如哥德爾完備性定理、哥德爾關於選擇公理一致性的證明、素數定理、各種安全協議的正確性、程式語言語義的特性。這些定理形式化工作的維護透過形式化證明存檔進行；截至 2019 年它已包含逾 500 個條目，兩百萬行證明。Isabelle 定理證明器是開源軟體，其原始碼在 BSD license 下授權釋出。“Isabelle”由其作者 Lawrence Paulson 命名；這名字取自於法國計算機科學家 的女兒。示例.Isabelle 支援兩種不同風格的的證明書寫方式：過程式和宣告式。過程式風格的證明主要由一系列證明策略或過程的依次運用組成；它能夠較好地反映數學家思考證明的過程，但通常較難閱讀，因為它無法直接體現每步推演的結果。宣告式風格的證明則與之相反，它以直接的方式描述了每一步確切的數學推演，因此較容易被閱讀和人工檢查。在較新版本的 Isabelle 中，過程式風格的證明已不建議再使用。形式化證明存檔亦推薦使用宣告式風格來書寫證明。例如，下面是一個宣告式風格的“2的算術平方根是無理數”的證明：theorem sqrt2_not_rational:"sqrt (real 2) ∉ ℚ"prooflet ?x = "sqrt (real 2)"assume "?x ∈ ℚ"then obtain m n :: nat wheresqrt_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^22 * n^2" using of_nat_eq_iff power2_eq_square by fastforcehence "2 dvd m^2" by simphence "2 dvd m" by simphave "2 dvd n" proof -from ‹2 dvd m› obtain k where "m2 * k" ..with eq have "2 * n^22^2 * k^2" by simphence "2 dvd n^2" by simpthus "2 dvd n" by simpqedwith ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest)with lowest_terms have "2 dvd 1" by simpthus False using odd_one by blastqed應用.除數學證明以外，Isabelle 亦被廣泛應用於計算機軟體及硬體的形式化驗證：Isabelle 的網站上有一個使用 Isabelle 的研究專案列表。拓展閱讀.
metadata: erhwenkuo/wikipedia-zhtw
metadata: Isabelle
metadata: https://zh.wikipedia.org/wiki?curid=6907754