imported>ExultantEditor 来自 2025年12月26日 (五) 17:42

2025-12-26T17:42:38Z

新页面

{{Infobox software
| name = Isabelle
| logo =
| screenshot = Isabelle jedit.png
| caption = 运行在 macOS 之上的 Isabelle/jEdit
| collapsible =
| author = {{le|Lawrence Paulson}}
| developer = [[剑桥大学]]、[[慕尼黑工业大学]]
| released = 1986<ref>{{Cite journal | doi = 10.1016/0743-1066(86)90015-4| title = Natural deduction as higher-order resolution| journal = The Journal of Logic Programming| volume = 3| issue = 3| page = 237| year = 1986| last1 = Paulson | first1 = L. C. | arxiv = cs/9301104}}</ref>
| latest release version = 2022
| latest release date =
| programming language = [[Standard ML]]、[[Scala]]
| operating system = [[Linux]]、[[Windows]]、[[macOS]]
| genre = [[数学]]
| license = [[BSD license]]
| website = {{url|https://isabelle.in.tum.de/}}
}}

'''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 个条目，两百万行证明。<ref>{{cite web |last1=Eberl |first1=Manuel |last2=Klein |first2=Gerwin |last3=Nipkow |first3=Tobias |last4=Paulson |first4=Larry |last5=Thiemann |first5=René |title=Archive of Formal Proofs |url=https://www.isa-afp.org/ |accessdate=22 October 2019 |ref=AFP |archive-date=2020-12-19 |archive-url=https://web.archive.org/web/20201219093338/https://www.isa-afp.org/ |dead-url=no }}</ref>

Isabelle 定理证明器是[[开源软件]]，其源码在 [[BSD license]] 下授权发布。

“Isabelle”由其作者 Lawrence Paulson 命名；这名字取自于法国计算机科学家 {{le|Gérard Huet}} 的女儿。<ref>{{cite web|url=http://www.cl.cam.ac.uk/~mjcg/Research94/node3.html|title=1.2 History|work=Isabelle and HOL|publisher=Cambridge AR Research (The Automated Reasoning Group)|last=Gordon|first=Mike|date=1994-11-16|access-date=2016-04-28|archive-date=2017-03-05|archive-url=https://web.archive.org/web/20170305020417/http://www.cl.cam.ac.uk/~mjcg/Research94/node3.html|dead-url=no}}</ref>

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

在较新版本的 Isabelle 中，过程式风格的证明已不建议再使用。形式化证明存档（Archive of Formal Proofs）亦推荐使用声明式风格来书写证明。<ref name="afp">{{cite web|title=Archive of Formal Proofs|url=https://www.isa-afp.org/|accessdate=2020-02-11|archive-date=2020-12-19|archive-url=https://web.archive.org/web/20201219093338/https://www.isa-afp.org/|dead-url=no}}</ref>

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

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

== 应用 ==
除数学证明以外，Isabelle 亦被广泛应用于计算机软件及硬件的[[形式化验证]]：
* 2009年，澳大利亚 [[NICTA]] 的 L4 团队开发了史上首个功能正确性得以形式化验证的通用[[操作系统]]内核：[[seL4]] [[微内核]]。其证明使用 Isabelle/HOL 构建，包含了 200000 行证明脚本，用以验证 7500 行 C 代码。该形式化验证涵盖了代码、设计与实现，其主定理指出：该内核的 C 代码正确地实现了其形式化设计规范。
* 程序语言 Lightweight Java 类型安全的形式化证明使用了 Isabelle。<ref>{{Cite web |url=http://afp.sourceforge.net/entries/LightweightJava.shtml |title=afp.sourceforge.net |accessdate=2020-02-11 |archive-date=2016-03-19 |archive-url=https://web.archive.org/web/20160319084033/http://afp.sourceforge.net/entries/LightweightJava.shtml |dead-url=no }}</ref>

Isabelle 的网站上有一个使用 Isabelle 的研究项目列表<ref>[https://isabelle.in.tum.de/community/Projects 使用 Isabelle 的研究项目列表] {{Wayback|url=https://isabelle.in.tum.de/community/Projects |date=20200412222424 }}</ref>。

== 参考文献 ==
{{Reflist}}

== 拓展阅读 ==
{{Refbegin}}
* [[Lawrence Paulson|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''.
{{Refend}}

== 外部链接 ==
* [https://isabelle.in.tum.de/ Isabelle 的官方网站] {{Wayback|url=https://isabelle.in.tum.de/ |date=20201130061048 }}
* [https://www.isa-afp.org/ 形式化证明存档（The Archive of Formal Proofs）] {{Wayback|url=https://www.isa-afp.org/ |date=20201219093338 }}
* [https://savannah.nongnu.org/projects/isarmathlib IsarMathLib] {{Wayback|url=https://savannah.nongnu.org/projects/isarmathlib |date=20200808013138 }}

[[Category:定理证明器]]
[[Category:函数式编程语言]]

Isabelle - 版本历史

imported>ExultantEditor 来自 2025年12月26日 (五) 17:42