自动定理证明

                     

贡献者： 待更新

　　 （本文根据 CC-BY-SA 协议转载自原搜狗科学百科对英文维基百科的翻译）

　　 自动定理证明(也称为自动推理证明或自动演绎)是自动推理和数学逻辑的一个分支，处理通过计算机程序来证明数学定理。数学证明的自动推理是计算机科学发展的主要推动力。

1. 逻辑基础

　　 虽然形式逻辑的根源可以追溯到亚里士多德，但在 19 世纪末和 20 世纪初，现代逻辑和形式数学得到了发展。弗雷格的 Begriffsschrift (1879)引入了完整的命题演算和本质上是现代谓词逻辑。[1] 他的《算术基础》发表于 1884 年，[2] 用形式逻辑表达了数学(的一部分)。罗素和怀特海在其颇具影响力的《数学原理》中延续了这种方法，该书于 1910-1913 年首次出版，[3] 并于 1927 年修订了第二版。[4] 罗素和怀特海认为，他们可以利用形式逻辑的公理和推理规则推导出所有的数学真理，原则上为自动化开辟了道路。1920 年，Thoralf Skolem 简化了 Leopold Löwenheim 先前的结果，从而得到了勒文海姆–斯科伦定理，并在 1930 年引入了 Herbrand universe 和 Herbrand interpretation 的概念，使得一阶公式(以及定理的有效性)的(不)可满足性被简化为(潜在无限多的)命题可满足性问题。[5]

　　 1929 年，Mojżesz Presburger 证明了带有加法和等式的自然数理论(现在以他的名字命名为普雷斯伯格算术)是可判定的，并给出了一个可以判定该语言中给定的句子是对还是错的算法。[6]然而，在这个积极的结果之后不久，Kurt Gödel 发表了《数学原理和相关系统的形式上不可判定的命题》(1931)，表明在任何足够强的公理系统中都有无法在系统中证明的真实陈述。这个话题在 20 世纪 30 年代由阿隆佐·邱奇和艾伦·图灵进一步发展，他们一方面给出了可计算性的两个独立但等价的定义，另一方面给出了不可判定问题的具体例子。

2. 第一次实现

　　 第二次世界大战后不久，第一台通用计算机问世了。1954 年，马丁·戴维斯为普林斯顿高等研究院的 JOHNNIAC 真空管计算机编程了普雷斯伯格算法。戴维斯认为，“它的伟大胜利是证明两个偶数的和是偶数”。[7][7] 更雄心勃勃的是 1956 年的逻辑理论机器，这是艾伦·纽厄尔、赫伯特·西蒙斯和约翰·肖为《数学原理》命题逻辑开发的演绎系统。逻辑理论机器也在 JOHNNIAC 上运行，它从一小组命题公理和三个演绎规则中构造证明:模分，(命题)变量替换，以及公式按其定义的替换。该系统使用启发式引导，并设法证明了原理的前 52 个定理中的 38 个。[7]

　　 逻辑理论机器的 “启发式” 方法试图模仿人类数学家，并且不能保证即使在原则上也能找到每个有效定理的证明。相比之下，其他更系统的算法至少在理论上实现了一阶逻辑的完备性。最初的方法依赖于 Herbrand 和 Skolem 的结果，通过用 Herbrand universe 中的项实例化变量，将一阶公式转换成相继更大的命题公式集。然后可以使用多种方法检查命题公式的不可满足性。Gilmore 的程序使用了到析取范式的转换，在析取范式中，公式的可满足性是显而易见的。[7][8]

3. 问题的可判定性

　　 根据基础的逻辑，决定公式有效性的问题从微不足道到不可能。对于命题逻辑的常见情况，问题是可判定的，但共 NP 完全的，因此一般证明任务只存在指数时间算法。对于一阶谓词演算，哥德尔完备性定理指出定理(可证明语句)完全是逻辑上有效的格式良好的公式，因此识别有效公式是递归可枚举的:给定无界资源，任何有效公式最终都可以被证明。然而，无效的公式(那些不属于给定理论的公式)不能总是被识别。

　　 以上适用于一阶理论，如 Peano 算法。然而，对于可以用一阶理论描述的特定模型，一些陈述可能是真实的，但是在用于描述模型的理论中是不可确定的。例如，通过哥德尔的不完全性定理，我们知道，对于自然数来说，任何一个适当公理为真的理论都不能证明所有一阶语句对于自然数都为真，即使允许正确公理的列表是无限可枚举的。因此，当所研究的陈述在所使用的理论中是不可判定的，即使在感兴趣的模型中是真实的，自动定理证明器在精确搜索证明时也将无法终止。尽管有这个理论上的限制，但在实践中，定理证明器可以解决许多难题，即使是在没有被任何一阶理论(如整数)完全描述的模型中。

4. 相关问题

　　 一个更简单但相关的问题是证明验证，即证明一个定理的现有证明是有效的。为此，通常要求每个单独的证明步骤都可以通过原始递归函数或程序来验证，因此问题总是可以判定的。

　　 由于自动定理证明器产生的证明通常非常大，证明压缩的问题至关重要，并且已经开发了各种旨在使证明器的输出更小，从而更容易理解和检查的技术。

　　 证明助理要求人类用户给系统提示。根据自动化程度的不同，证明器本质上可以简化为一个证明检查器，用户以正式的方式提供证明，或者重要的证明任务可以自动执行。交互式证明器被用于多种任务，但即使是全自动系统也已经证明了许多有趣而又困难的定理，包括至少一个人类数学家长期回避的定理，即罗宾斯猜想。[9][10] 然而，这些成功是零星的，解决难题通常需要熟练的用户。

　　 定理证明和其他技术之间的另一个区别是，如果一个过程由传统的证明组成，那么这个过程被认为是定理证明，从公理开始，使用推理规则产生新的推理步骤。其他技术包括模型检查，在最简单的情况下，它涉及许多可能状态的暴力枚举(尽管模型检查器的实际实现需要很多聪明，而不仅仅是暴力)。

　　 有混合定理证明系统使用模型检查作为推理规则。也有一些程序是为了证明一个特定的定理而编写的，并且（通常是非正式的）证明如果程序以某个结果结束，那么这个定理就是真的。这方面的一个很好的例子是四色定理的机器辅助证明，这是第一个声称的数学证明是非常有争议的，由于程序计算的巨大规模，人类基本上无法对其进行验证(这种证明被称为不可测量的证明)。程序辅助证明的另一个例子是显示第一个玩家总是可以赢得 Connect Four 的游戏。

5. 工业用途

　　 自动化定理证明的商业应用主要集中在集成电路设计和验证上。自从奔腾 FDIV 错误以来，现代微处理器的复杂浮点单元已经被设计得非常仔细。AMD、英特尔和其他公司使用自动定理证明来验证除法和其他操作在他们的处理器中是否正确实现。

6. 一阶定理证明

　　 20 世纪 60 年代末，资助自动演绎研究的机构开始强调实际应用的需求。第一个富有成果的领域之一是程序验证，一阶定理证明器被应用于用 Pascal, Ada, Java 等语言验证计算机程序正确性的问题。早期程序验证系统中值得注意的是斯坦福大学 David Luckham 开发的斯坦福 Pascal 验证器。这是基于在斯坦福使用 John Alan Robinson 的分辨率原理开发的斯坦福分辨率证明器。这是第一个展示解决数学问题能力的自动演绎系统，该系统在解决方案正式发布之前就已经在美国数学学会的公告中公布了。

　　 一阶定理证明是自动化定理证明中最成熟的子领域之一。这种逻辑表达能力足够强，允许以合理自然和直观的方式描述任意问题。另一方面，它仍然是半可判定的，并且已经开发了许多可靠的完整的计算，从而使全自动系统成为可能。更具表现力的逻辑，如高阶逻辑，可以方便地表达比一阶逻辑更广泛的问题，但是这些逻辑的定理证明还不太完善。

7. 基准、竞争和来源

　　 已实现系统的质量得益于大量标准基准示例的存在——定理证明器(TPTP)问题库的成千上万个问题[11] ——以及来自 CADE ATP 系统竞赛(CASC)，CASC 是一阶系统对许多重要一阶问题的年度竞赛。

　　 下面列出了一些重要的系统(都赢得了至少一个 CASC 竞赛部门)。

• E 是全一阶逻辑的高性能证明器，但建立在纯方程式演算的基础上，最初由慕尼黑工业大学的自动推理小组开发，现在位于斯图加特的巴登-符腾堡合作州立大学。
• Otter 是在阿尔贡国家实验室开发的，基于一阶分辨率和调优。Otter 后来被 Prover9 取代，Prover9 与 Mace4 配对。
• SETHEO 是一个基于目标导向模型消除演算的高性能系统。它是由慕尼黑工业大学的自动推理小组开发的。E 和 SETHEO 已经在复合定理证明器 E-SETHEO 中与结合（其他系统）使用。
• Vampire 是 Andrei Voronkov 和 Krystof Hoder 在 Manchester University 开发和实现的，之前也由 Alexandre Riazanov 开发和实施。11 年来(1999 年、2001 年至 2010 年)，它在最负盛名的 CNF 赛区赢得了 CADE ATP 系统竞赛。
• Waldmeister 是 Arnim Buch 和 Thomas Hillenbrand 开发的单位方程一阶逻辑的专门系统，它连续十四年(1997-2010 年)获得 CASC UEQ 赛区冠军。
• SPASS 是具有等式的一阶逻辑定理证明器。这是由马克斯·普朗克计算机科学研究所逻辑自动化研究小组开发的。

　　 Theorem Prover Museum 是一项保护定理证明器系统的资源以备将来分析的举措，因为它们是重要的文化/科学人工文物。它有上述许多系统的来源。

8. 流行技术

• 具有统一性的一阶分辨率
• 模型消除
• 分析表格法
• 叠加和术语重写
• 模型检查
• 数学归纳法[12]
• 二元决策图
• DPLL
• 高阶统一

9. 软件系统

9.1 免费软件

• Alt-Ergo
• 自动数学
• CVC
• E([2])
• 哥德尔机
• iProver
• IsaPlanner
• KED 定理证明者[13]
• leanCoP[14]
• Leo II([3])
• LCF
• LoTREC[15]
• MetaPRL[16]
• Mizar
• NuPRL
• 悖论
• 简化(GPL'ed since 5/2011)
• Twelf
• SPARK（编程语言）

9.2 专有软件

• Acumen 规则管理器(商业产品)
• ALLIGATOR (CC BY-NC-SA 2.0 UK)
• CARINE
• KIV (作为 Eclipse 的插件免费提供)
• Prover Plug-In (商业证明引擎产品)
• ProverBox
• Wolfram Mathematica[17]
• ResearchCyc
• 矛模算术定理证明器

10. 名人

• Leo Bachmair，叠加演算的共同开发者
• Woody Bledsoe，人工智能先驱
• Robert S. Boyer，《Boyer-Moore 定理证明》的合著者，1999 年 Herbrand 奖的共同获奖者
• Alan Bundy，爱丁堡大学，指导归纳证明的元级推理、证据规划和 2007 年 IJCAI 卓越研究奖、Herbrand 奖和 2003 年 Donald E. Walker 杰出服务奖获得者
• William McCune，阿贡国家实验室，Otter 的作者，第一个高性能定理证明者，许多重要论文，2000 年 Herbrand 奖的获得者
• Hubert Comon，CNRS 和现在的 ENS Cachan，许多重要的论文
• 康奈尔大学 Robert Lee Constable，类型理论的主要贡献者，NuPRL 系统的主要开发者文
• Martin Davis，《人工推理手册》的作者，DPLL 算法的共同发明人，2005 年 Herbrand 奖的获得者
• 加州大学伯克利分校的 Branden Fitelson 致力于自动发现逻辑系统的最短公理基础
• Harald Ganzinger，叠加演算的共同开发者，MPI Saarbrücken 的负责人，2004 年 Herbrand 奖(死后)的获得者
• Michael Genesereth 斯坦福大学计算机科学教授
• Melvin Fitting，ATP 的几本书和几百篇文章的作者，画面证明系统软件研究员
• Keith Goolsbey，Cyc 推理机的主要开发者
• Michael J. C. Gordon 领导了 HOL 定理证明器的开发
• Gérard Hue，术语重写，HOL 逻辑，1998 年 Herbrand 奖
• Robert Kowalski 开发了连接图定理证明器和 SLD 解析器，这是执行逻辑程序的推理机
• Donald W. Loveland 杜克大学，作者，DPLL 程序的共同开发者，模型消除的开发者，2001 年 Herbrand 奖的获得者
• 斯坦福大学的 David Luckham 开发了斯坦福解析定理证明器 1968，这是第一个用于解决 AMS 通知中宣布的问题的自动演绎系统，随后开发了斯坦福 Pascal 验证器、第一个 Pascal 程序验证系统和一个广泛分布的程序验证系统，1968-75
• Norman Megill，元数学的开发者，也是它在 metamath.org 网站的维护者，这是一个自动验证证明的在线数据库
• J Strother Moore，《Boyer–Moore 定理证明》的合著者，1999 年 Herbrand 奖的获得者
• 巴塞罗那大学 Robert Nieuwenhuis，叠加演算的共同开发者
• 慕尼黑技术大学的 Tobias Nipkow，对(高阶)重写的贡献，Isabelle 证明助理的共同开发者
• Ross Overbeek，阿贡国家实验室，基因组解释研究会的创始人 The Fellowship for Interpretation of Genomes
• 剑桥大学的 Lawrence C. Paulson 研究高阶逻辑系统，Isabelle 定理证明器的共同开发者
• 位于教堂山的北卡罗来纳大学大卫·普莱斯特分校，复杂性结果，对重写和完成的贡献，基于实例的定理证明
• John Rushby，斯坦福国际研究院的项目总监[18]
• 锡拉丘兹大学的 J. Alan Robinson 开发了基于原始解析和统一的一阶定理证明，他是《自动推理手册》的联合编辑，1996 年获得了 Herbrand 奖
• Jürgen Schmidhuber，关于歌德尔机器的研究：自我指导的通用问题解决方案，实现了最佳的自我改进 Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements
• Stephan Schulz, E 定理证明者
• 斯坦福国际研究所的 Natarajan Shankar 致力于决策程序、小证明引擎、PVS 的共同开发者
• Mark Stickel，斯坦福国际研究院，2002 年 Herbrand 奖获得者
• Geoff Sutcliffe，迈阿密大学，TPTP 系列的维护者，CADE 年度比赛的组织者
• 普渡大学的 Dolph Ulrich 致力于系统最短公理基础的自动发现
• Robert Veroff 新墨西哥大学，许多重要论文
• Andrei Voronkov，Vampire 的开发者和《自动推理手册》的联合编辑
• 克里斯托弗·韦登巴赫，自动定理证明器 SPASS 的作者
• Larry Wos，阿贡国家实验室(Otter)，许多重要论文，第一个 Herbrand 奖获得者(1992 年)
• 吴文俊，几何定理证明工作:吴方法，1997 年 Herbrand 奖

11. 参考文献

　　 [1] ^Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert..

　　 [2] ^Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 2007-09-26. Retrieved 2012-09-02..

　　 [3] ^Bertrand Russell; Alfred North Whitehead (1910–1913). Principia Mathematica (1st ed.). Cambridge University Press..

　　 [4] ^Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2nd ed.). Cambridge University Press..

　　 [5] ^Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration..

　　 [6] ^Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101..

　　 [7] ^Davis, Martin (2001), "The Early History of Automated Deduction", in Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning, 1, Elsevier).

　　 [8] ^Gilmore, Paul (1960). "A proof procedure for quantification theory: its justification and realisation". IBM Journal of Research and Development. 4: 28–35. doi:10.1147/rd.41.0028..

　　 [9] ^W.W. McCune (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881..

　　 [10] ^Gina Kolata (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. Retrieved 2008-10-11..

　　 [11] ^Sutcliffe, Geoff. "The TPTP Problem Library for Automated Theorem Proving". Retrieved 8 September 2012..

　　 [12] ^Bundy, Alan. The automation of proof by mathematical induction. 1999..

　　 [13] ^Artosi, Alberto, Paola Cattabriga, and Guido Governatori. "Ked: A deontic theorem prover." Eleventh International Conference on Logic Programming (ICLP’94). 1994..

　　 [14] ^Otten, Jens, and Wolfgang Bibel. "leanCoP: lean connection-based theorem proving." Journal of Symbolic Computation 36.1-2 (2003): 139-161..

　　 [15] ^del Cerro, Luis Farinas, et al. "Lotrec: the generic tableau prover for modal and description logics." International Joint Conference on Automated Reasoning. Springer, Berlin, Heidelberg, 2001..

　　 [16] ^Hickey, Jason, et al. "MetaPRL–a modular logical environment." International Conference on Theorem Proving in Higher Order Logics. Springer, Berlin, Heidelberg, 2003..

　　 [17] ^[1] Mathematica documentation.

　　 [18] ^"SRI International Computer Science Laboratory – John Rushby". SRI International. Retrieved 22 September 2012..