自动定理证明

虽然形式逻辑的根源可以追溯到亚里士多德，但在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年代由阿隆佐·邱奇和艾伦·图灵进一步发展，他们一方面给出了可计算性的两个独立但等价的定义，另一方面给出了不可判定问题的具体例子。

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

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

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

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

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

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

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

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

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

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

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

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

已实现系统的质量得益于大量标准基准示例的存在——定理证明器(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 是一项保护定理证明器系统的资源以备将来分析的举措，因为它们是重要的文化/科学人工文物。它有上述许多系统的来源。

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

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
• 矛模算术定理证明器

• 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奖