自动化定理证明

自动化定理证明（也称为 ATP 或自动演绎）是自动推理和数学逻辑的一个子领域，涉及通过计算机程序证明数学定理。 基于数学证明的自动推理是计算机科学发展的主要推动力。

虽然形式化逻辑的根源可以追溯到亚里士多德，但在 19 世纪末和 20 世纪初见证了现代逻辑和形式化数学的发展。 弗雷格的 Begriffsschrift (1879) 介绍了完整的命题演算和现代谓词逻辑的本质。 他的 Foundations of Arithmetic 于 1884 年出版，用形式逻辑表达了（部分）数学。 罗素和怀特海在他们颇具影响力的《数学原理》中继续采用这种方法，该书于 1910 年至 1913 年首次出版，并于 1927 年修订了第二版。罗素和怀特海认为他们可以使用形式逻辑的公理和推理规则推导出所有数学真理，原则上 开放流程以实现自动化。 1920 年，Thoralf Skolem 简化了 Leopold Löwenheim 先前的结果，得出了 Löwenheim-Skolem 定理，并在 1930 年提出了 Herbrand 宇宙的概念和 Herbrand 解释，该解释允许（不）满足一阶公式（因此 一个定理的有效性）被简化为（可能是无限多的）命题可满足性问题。

1929 年，Mojżesz Presburger 证明了加法和相等的自然数理论（现在以他的名义称为 Presburger 算术）是可判定的，并给出了一种算法，可以确定语言中给定的句子是真还是假。然而，不久之后 库尔特·哥德尔 (Kurt Gödel) 发表了《数学原理及相关系统的形式上不可判定的命题》(On Formally Undecidable Propositions of Principia Mathematica and Related Systems) (1931)，表明在任何足够强的公理系统中，都存在无法在系统中证明的真陈述。 这个话题在 1930 年代由 Alonzo Church 和 Alan Turing 进一步发展，他们一方面给出了两个独立但等价的可计算性定义，另一方面给出了不可判定问题的具体例子。

1954 年，Martin Davis 在新泽西州普林斯顿高等研究院为 JOHNNIAC 真空管计算机编写了 Presburger 算法。 根据戴维斯的说法，它的伟大胜利是证明了两个偶数之和是偶数。 更雄心勃勃的是 1956 年的逻辑理论机，这是一个用于数学原理命题逻辑的演绎系统，由 Allen Newell、Herbert A. Simon 和 J. C. Shaw 开发。 同样在 JOHNNIAC 上运行的逻辑理论机从一小组命题公理和三个演绎规则构建证明：先决条件、（命题）变量替换，以及通过定义替换公式。 该系统使用启发式指导，成功证明了《原理》前 52 个定理中的 38 个。

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

根据底层逻辑，决定公式有效性的问题从微不足道到不可能。 对于命题逻辑的常见情况，问题是可判定的但 co-NP-complete，因此一般证明任务只存在指数时间算法。 对于一阶谓词演算，哥德尔的完备性定理指出定理（可证明的陈述）恰好是逻辑上有效的格式正确的公式，因此识别有效公式是递归可枚举的：给定无限资源，任何有效公式最终都可以被证明 . 然而，无效的公式（给定理论未包含的公式）并不总能被识别。