2.2.1 自动定理证明的起源、发展与现状
第一个可运行的定理证明程序是1954 年由逻辑学家Martin Davis完成，实现了普利斯伯格算术(Presburger Arithmetic)的判定过程[68] 。自然数的一阶理论又称皮亚诺算术，包括自然数的加法和乘法，普利斯伯格算术是皮亚诺算术的一个子集，只有加法没有乘法。皮亚诺算术不可判定，但普利斯伯格算术则是可判定的。这个证明器证明了“两个偶数之和还是偶数”。
1956 年的达特茅斯人工智能讨论会议被认为是人工智能研究领域的起源。讨论会上，Newell 和 Simon 发表《逻辑理论机》（The Logic
Theory Machine），被认为是自动定理证明（Automated Theorem Proving， ATP）领域的第一篇论文[69] 。逻辑理论机的目标是想机械地模仿人 类在证明命题逻辑时所用的推导过程，它可以证明怀海特和罗素《数 学原理》第一卷中命题逻辑部分的一个很大的子集。
1957 年 Dag Prawwitz 和他父亲编程实现了根岑 Gentzen 提出的自然演绎，发表了影响深远的论文，在论文中提出合一的概念[70] 。
1959 年 IBM 的 Gelernter 等人实现几何定理证明器[71] 。该系统 采用“反向链”的推理方法，从目标开始向前提产生新的子目标，这 些子目标逻辑蕴涵最终目标。几何定理证明器能够证明直线图形中的 大部分高中考试的问题，并且运行时间也常常与高中生解题时间近似。
同年，与 Gelernter 同项目组的同事 Gilmore 实现了基于语义表 (Semantic Tableau)方法的定理证明器，被认为是对谓词演算的第一个可用的机械证明程序[72] 。
1958 年至 1960 年间，王浩先后实现了三个 ATP 程序[73] ：一个完全的命题逻辑程序，一个谓词逻辑程序及其改进。其改进的谓词逻辑程序在 40 分钟内证明了《数学原理》中全部的 150 条谓词逻辑以
及 200 条命题逻辑定理。王浩的这项工作说明让机器拥有人类的技巧已不再是一种游戏。
Gilmore 方法的理论基础是 Herbrand 定理：为证明某谓词逻辑公式的恒假性，转化为去证明该谓词逻辑公式在 Herbrand 域上实例化得到的命题公式的恒假性[75] 。在证明命题公式恒假性时，Gilmore 采用了最原始的“乘法方法”。
1960 年，Martin Davis 和 Hilary Putnam 对 Gilmore 方法做了改进，提出所谓的 D-P 过程[76] ，后进化为当前使用的 DPLL 过程[77] 。但是，D-P 过程对Gilmore 方法的改进不是本质的，因为这两种方法，都需要枚举基替换，去产生恒假的命题公式。
1960 年 Dag Prawitz 发表论文，指出 D-P 过程的这个致命弱点，
并给出了改进[70] 。Prawitz 不再枚举替换去产生恒假的命题公式，而是主动去寻找产生这个恒假命题公式的那个替换。Prawitz 的“直接寻找替换，从而避免产生公式的组合爆炸”这种思想是深刻的，使用了人工智能中的匹配技术。但 Prawitz 在实现这种想法时，效果却很不理想。
1960 年前后的三年间，是自动定理证明领域中逻辑方法的一段重要时间。基于 Herbrand 定理的Gilmore 方法，D-P 过程，尤其是 D- P 过程中的单文字规则和 Prawitz 的匹配思想，最终导致归结原理的产生。
1964 年 J.A.Robinson 提出简洁而漂亮的归结原理[78] 。被 Robinson 用归结原理所形式化的逻辑里，没有公理，只有一条使用合一替换的推导规则。而如此简洁的逻辑系统，却是谓词演算中的一个完备系统：任意一个恒真的一阶公式，在 Robinson 的逻辑系统中都是可证的。
重要的改进工作包含：
1964 年 Wos，Carson 和 G. Robinson 提出了单文字子句优先处理
[79] 和支撑集策略[80] 。1965 年 J.A.Robinson 提出超归结方法。1967年提出语义归结[81] 。1968 年Loveland 和Luckham提出线性归结[82] 。 1970 年Boyer 提出锁归结。1970 年提出 SL-归结[83] ，被用于早期的 PROLOG 语言中。1970 年 C.L.Chang 提出输入归结，并证明其和单元归结等价[84] 。1982 年 Murray 提出 NC（Non-Clausal）归结[85] 。
相等是数学中重要且常见的概念，对于包含等词的公式进行推理 需要特殊的规则：Wos 等人提出 Paramodulation 调解方法[86] ，调解 方法被推广为superposition 方法，成为现代定理证明器的理论和实践 基础[88] 。方程式（等式）是一阶逻辑的子集，即只有一个谓词 EQUAL。 BirkHoff 证明了方程逻辑是完全的。在项重写[89] 中，证明就是将一 个符号串（实际上是谓词逻辑中的项）根据给定的等式重写成另一符
号串。为减少生成的项的数量，引入项之间的序关系来限制重写。 Knuth-Bendix Ordering 是上世纪七十年代提出的用于项重写的主要技术[90] 。
上世纪八十年代后，自动定理证明领域没有突破性的进展，但该方向逐渐改名为自动推理，希望计算机程序成为一种工具，能够自动完成各种需要的推理任务。 自动推理领域的归结会议是 CADE(Conference of Automated DEduction)[91] 和 IJCAR(International Conference of Automated Reasoning)[92] ，它们都是双年会议，每年两个会议交替召开。CASC (CADE ATP System Competition) 是至今每年仍在 CADE 或 IJCAR 会议上举办的自动定理证明系统比赛[93] ，赛题来自TPTP (Thousands Problems for Theorem Provers)，TPTP 是定理证明器的公认的benchmark[94] 。历年的CASC 冠军中包括Otter[95] , Vampire[96] 等著名定理证明器。归结原理导致的组合爆炸仍然需要启发式方法的帮助，定理证明领域陷入停滞状态。近年，谷歌团队的实验表明，简单的卷积神经网络可以帮助定理证明器挑选子句从而提高性能[97] 。
另一方面，研究者们在几何定理证明与计算机代数方向取得比较满意的结果，代表性的工作为吴文俊院士在上世纪七十年代针对特定初等几何问题得到高效的算法[98] ，并且被推广到一类微分几何问题上[99] 。