1 历史与背景
1.1 早期探索（20世纪50–60年代）
自动定理证明的起源可追溯至人工智能与数理逻辑的结合初期。20世纪50年代，随着现代计算机的诞生，研究者开始尝试将人类数学推理过程转化为机械化的符号操作。
1.1.1 逻辑理论机（Logic Theorist）
1956年，艾伦·纽厄尔（Allen Newell）、赫伯特·西蒙（Herbert Simon）和约翰·克里夫·肖（John Cliff Shaw）开发了历史上第一个自动定理证明程序——逻辑理论机（Logic Theorist）。该程序能够证明《数学原理》（Principia Mathematica）中前52条命题中的38条，其核心方法基于启发式搜索，模拟人类数学家尝试简化目标再回溯的策略。逻辑理论机被认为是人工智能领域的里程碑式成果，直接催生了后来被称为"物理符号系统假说"的研究方向。
1.1.2 归结原理的提出
1965年，约翰·艾伦·罗宾逊（John Alan Robinson）发表了划时代论文，提出了归结原理（Resolution Principle）。该原理将一阶逻辑的推理过程简化为单一规则——通过寻找互补文字（Literals）对子句进行消解，从而生成新的子句。归结原理的完备性（即若公式不可满足，则通过反复归结必能导出空子句）为自动定理证明奠定了坚实的数学基础。与前向搜索策略相比，归结原理显著减少了推理规则的种类，使机器可以在统一的框架下处理全称量化与存在量化。
1.2 黄金发展期（20世纪70–90年代）
归结原理的提出引发了ATP领域的爆发式增长，大量基于归结的系统和策略在此期间涌现。
1.2.1 超级归结与参数化策略
1970年代，研究者发现原始归结在处理等式推理时效率极低。超级归结（Superposition）应运而生，它结合了重写（Rewriting）与定向等式替换，通过有序地应用等式单位对子句进行规范形变换。同时，参数化策略（Paramodulation）开始被用于处理带有等式的自动证明，其基本思想是允许将等式中的一侧替换为另一侧，而无需先将等式转化为子句形式。
1.2.2 交互式定理证明器的兴起
1980年代，纯自动化证明的局限性逐渐显现——很多有实际意义的定理（尤其是涉及复杂归纳或高阶逻辑的问题）很难被彻底自动解决。为此，以LCF（Logic for Computable Functions）为代表的交互式证明助手诞生了。LCF采用了"可信内核"（Trusted Kernel）架构：用户通过编写策略（Tactics）引导证明，而内核仅执行一组极小化的简单推理规则。这种设计既保证了证明的正确性，又让人类专家能够介入关键步骤。随后出现的HOL、Isabelle、Coq等系统均沿袭了这一范式。
1.3 现代进展（21世纪至今）
进入21世纪，ATP领域呈现出与机器学习、大规模库融合的趋势。
1.3.1 机器学习与证明搜索的结合
传统的ATP搜索常陷入"组合爆炸"困境——每一步可选择的推理规则以指数级增长。近年，研究者利用神经网络（如图神经网络、Transformer）预测哪些子句或策略更可能导向成功证明。例如，LearnSAT 使用强化学习指导回溯，ENIGMA 系统则基于决策树或神经网络对子句进行评价，大幅提升了Vampire等ATP系统的效率。
1.3.2 大规模形式化数学库（如Mizar、Isabelle）
形式化数学库的出现使ATP不仅用于逻辑验证，更成为数学研究的一部分。Mizar 项目始于1973年，至今已形式化超过数万个数学定理，其语言接近自然数学风格。Isabelle 的 Archive of Formal Proofs（AFP） 收录了从组合数学到计算机理论的大量验证条目。这些库为ATP提供了高质量的测试基准，同时推动着自动化技术向更复杂的数学领域渗透。
2 基础理论
2.1 一阶逻辑与希尔伯特系统
自动定理证明的逻辑基础主要建立在一阶逻辑（First-Order Logic，FOL）之上。一阶逻辑允许使用变元、谓词、量词（∀与∃）以及函数符号，表达能力远强于命题逻辑。
2.1.1 命题逻辑的完备性
命题逻辑是自动定理证明的基石，其判定问题可解（即存在判断任意公式是否永真的算法）。真值表法或语义树法可以在有限时间内完成判定。更关键的是，命题逻辑在经典语义下具有完备性：所有永真公式均可通过有限的推理步骤（如自然演绎或希尔伯特系统的公理模式）导出。
2.1.2 一阶逻辑的不可判定性
与命题逻辑不同，一阶逻辑的判定问题是不可判定的——不存在总能正确判断任意一阶逻辑公式是否为永真式的通用算法。这一结论由阿隆佐·丘奇（Alonzo Church）和艾伦·图灵（Alan Turing）在1936年独立证明，其本质是图灵机停机问题的一种编码。这意味着任何ATP系统在一阶逻辑层面都必然存在"遇到不可解问题无限时间运行"的情况，因此实际系统中需要引入时间限制或搜索深度上限。
2.2 归结原理
归结原理是一阶逻辑ATP最核心的推理机制，它通过反证法来证明定理：要证明公式A是定理，只需证明其否定（¬A）与已知公理构成的集合不可满足。
2.2.1 子句形式与Skolem化
一阶逻辑公式在应用归结前需转换为子句合取范式（Conjunctive Normal Form，CNF）。转换过程包括：
- 消去蕴含（→）与等价（↔）；
- 将否定符号向内推直至仅作用于原子公式；
- 对存在量词进行Skolem化：用新的常数或函数符号（称为Skolem函数）替换存在量词约束的变元，从而消去全部存在量词；
- 最后将全称量词前置并将公式拆分为若干子句（子句即文字的析取）。
2.2.2 二元归结与因子归结
二元归结（Binary Resolution）指两个子句（分别包含互补文字L和¬L）通过统一替换（Unification）生成新子句的过程。例如，子句C1 = P(x) ∨ Q(x) 与 C2 = ¬P(a) ∨ R(y) 可通过统一{x/a}得到归结子句 Q(a) ∨ R(y)。
因子归结（Factoring）用于简化子句中重复的文字：如果一个子句的若干文字可通过统一变为相同，则可将它们合并为一个。例如，子句 C = P(x) ∨ P(f(y)) 可通过统一{x/f(y)}化为 P(f(y))，以避免冗余推理。
2.2.3 删减策略（纯字句删除、重言式删除等）
为了提高归结效率，系统在搜索过程中会大量删除冗余子句：
- 纯字句删除：如果一个文字在集合中没有互补文字，则该子句为"纯"的，可被删除而不影响不可满足性。
- 重言式删除：所有形式为 L ∨ ¬L ∨ ... 的子句（即同时包含一个文字及其否定）自动为真，因此可被移除。
- 子句包含（Subsumption）：若一个子句C1比C2"更一般"（即存在替换σ使得σ(C1) ⊆ C2），则可删除C2。
2.3 自然演绎与sequent演算
除归结外，ATP还常采用自然演绎（Natural Deduction）或sequent演算（Sequent Calculus）作为推理基础。这些方法更贴近人类数学证明的直觉：从前提和假设出发，运用引入/消除规则逐步推导结论。
2.3.1 直觉主义与经典逻辑的差异
自然演绎中，直觉主义逻辑与经典逻辑的核心分歧在于排中律（¬P ∨ P）和双重否定消去（¬¬P → P）是否被接受。直觉主义要求证明必须构造性地指出证据，而经典逻辑允许使用反证法。大多数ATP系统采用经典逻辑（如归结原理固有地依赖反证法），但某些系统（如基于类型论的证明助手Coq）默认使用直觉主义，并允许用户显式添加经典公理。
2.3.2 结构规则与cut消除
在sequent演算中，结构规则（如弱化、收缩）控制着上下文中公式的增删，而cut规则允许通过中间引用来连接证明片段。cut消除定理（Gerhard Gentzen的割消除定理）指出，任何包含cut的证明均可转化为无cut的证明，这为自动搜索提供了美学上的简洁性（无冗余步骤）。然而，实际ATP中保留cut往往可以缩短证明长度，因此割消除常被用作理论完备性工具而非实际搜索策略。
3 主要算法与技术
3.1 基于搜索的证明策略
归结原理的证明搜索本质上是在子句图（Resolution Graph）中寻找从初始子句到空子句的路径。
3.1.1 深度优先搜索与宽度优先搜索
最简单的策略是深度优先搜索（DFS）：每次选择最新生成的子句进行推理，直到找到空子句或达到深度限制。DFS空间节省，但易陷入无休止的"无意义"路径。宽度优先搜索（BFS）则逐层展开所有可能归结，保证了最短证明的发现，但内存消耗极大，实际中很少使用纯BFS。更常见的做法是利用迭代加深（Iterative Deepening DFS），在DFS上叠加深度限制并逐步放宽。
3.1.2 支持集策略（set-of-support）
支持集策略（Set of Support，SOS）是第一种被广泛使用的启发式策略，由Larry Wos等人提出。其核心思想是将初始子句分为两组：公理集（Axioms）和支持集（SOS），其中SOS是目标公式的否定以及相关子句。在推理过程中，每次归结必须至少有一个前提来自SOS；新生成的子句自动加入SOS。这样可以有效避免公理之间无意义的"自相残杀"，将搜索集中在与目标关系最密切的子句上。
3.2 超级归结（Superposition）
超级归结是处理等式理论（如群论、环论等）的最有效方法之一。
3.2.1 等式推理与重写
传统归结将等式表示为二元谓词（如Eq(a,b)），但这样会遗漏等式的代入能力。参量模化（Paramodulation）通过将等式一侧替换为另一侧来模拟等式的功能性，而超级归结对其进行了系统化改进，使其在与有序重写结合时更加高效。
超级归结的核心规则：若有两个子句C1: l = r ∨ ... 和 C2: s[t] ∨ ...，且存在替换σ使σ(l) = σ(t)，则可生成σ(s[r]) ∨ ...（即用r替换t）。注意，这里的t是s的一个子项。
3.2.2 有序重写与定向等式
为使超级归结高效，等式通常需被定向（Oriented），即按照某种项序（如KBO、LPO）规定较小的项替换较大的项。例如，若定义项序使其优先看重函数符号的"重量"，则x+0 = x可被定向为x+0 → x，而x = x+0则不被允许作为化简方向。定向保证了重写过程的终止性（即不会出现无限循环替换）。
3.3 SMT求解与可满足性模理论
可满足性模理论（Satisfiability Modulo Theories，SMT）是ATP的重要延伸，它处理带有特定理论背景（如整数算术、数组、位向量）的公式。
3.3.1 DPLL(T)框架
大多数现代SMT求解器（如Z3、CVC5）基于DPLL(T)框架。该框架将布尔部分与理论部分解耦：
- 一个DPLL风格的SAT求解器负责处理命题骨架（即公式的布尔结构）；
- 一套理论求解器（T-solver）负责检查命题赋值在特定理论下是否一致；
- 两者通过"引理学习"交互：当命题赋值导致理论矛盾时，理论求解器返回一个冲突子句，SAT求解器据此回溯。
3.3.2 理论与布尔传播的协同
效率的关键在于早检测（Early conflict detection）。理论求解器不仅被动等待SAT求解器完成赋值，还可以主动进行理论传播（Theory Propagation）：例如，在整数算术中，若已赋值为x>5且x<3，理论求解器可立即宣告矛盾并生成新子句¬(x>5) ∨ ¬(x<3)，从而提前驱动SAT回溯。
3.4 高阶定理证明与λ-Prolog
经典ATP主要面向一阶逻辑，而高阶逻辑（允许量化函数与谓词）的自动化更具挑战性。
3.4.1 类型论基础
高阶逻辑的自动化通常建立在类型论（Type Theory）之上。典型系统如λ-Prolog、Twelf等使用λProlog语言，其内在支持高阶统一、高阶假设以及模块化编程。类型论将"公式"与"证明"统一在同一个语法范畴中（Curry-Howard同构）：命题对应于类型，证明对应于类型中的项。这为高阶定理证明提供了光滑的计算基础。
3.4.2 高阶统一与模式匹配
高阶逻辑中，变量可以是谓词（如P(x)），因此统一操作需要处理变量作用域与λ-抽象。高阶统一（Higher-Order Unification）比一阶统一复杂得多（甚至不可判定），但高阶模式统一（Huet's Patterns）的受限形式是可判定的。λ-Prolog等系统正是利用这种受限模式来保证搜索的可管理性。
4 代表性系统
4.1 经典ATP系统
4.1.1 Otter与Prover9
Otter由William McCune于1980–1990年代在阿贡国家实验室开发，是历史上最著名的归结式ATP系统之一。它支持多种搜索策略（包络、支持集等），曾成功证明代数领域的多个公开问题（如罗宾斯代数猜想）。其后续版本Prover9（2000年代）增加了更现代的用户界面和更优的等式推理策略。
4.1.2 E（Equational Theorem Prover）
E由Stephan Schulz开发，是一款面向等式推理的高性能ATP系统。它在CASC（ATP系统竞赛）中屡获佳绩，核心特色是先进的字句排序（Clause Selection）机制，使用基于年龄和权重的优先级队列，并结合子句删除索引（如完美哈希）来实现极速的预处理。
4.1.3 Vampire（基于超级归结）
Vampire由Andrei Voronkov及其团队开发，是目前最强大的通用ATP系统之一。它融合了超级归结、实例生成（InstGen）以及前沿的机器学习指导策略。Vampire的另一特色是结果重证明（Proof Replay）：当发现解时，它会产生一个紧凑的证明，而后可由其他验证器（如Isabelle）进行独立验证。
4.2 交互式证明助手中的ATP组件
4.2.1 Isabelle/Sledgehammer
Sledgehammer是Isabelle交互式证明助手中的"锤子"工具。用户只需在证明中标记一个目标，Sledgehammer会自动将其转化为一阶逻辑，并调用后台多个ATP系统（如Vampire、E、Z3）进行搜索。若找到证明，它还会尝试将证明反译回Isabelle的战术（tactic）语言，从而极大简化了形式化验证工作。
4.2.2 Coq的自动策略（auto, omega等）
Coq提供一系列内置的自动策略：auto基于可调用的归纳纲要进行搜索；omega专门处理线性算术问题；congruence处理等式与全等关系。更强大的firstorder策略试图解决一阶逻辑目标，而zify则可将整数问题转化为SMT求解器可处理的格式。虽然这些策略的自动化程度低于专用ATP，但它们在Coq内部的"优雅环境"中运行，避免了不同系统之间的编码转换开销。
4.3 特殊领域系统
4.3.1 ACL2（基于重写与归纳）
ACL2（A Computational Logic for Applicative Common Lisp）是一个面向Lisp程序的形式化验证系统，其核心推理方法是重写和数学归纳。ACL2不要求目标完全自动完成，而是通过策略（如:induct、:cases）引导用户，同时利用精心编写的重写规则库自动完成大量个案推理。它成功应用于验证AMD、Intel等微处理器的浮点运算单元，以及NASA的飞行算法。
4.3.2 Z3（主要面向SMT，亦支持ATP）
Z3由微软研究院开发，是当今最广泛使用的SMT求解器之一。虽然其强项在于带有理论背景的布尔公式求解，但其内置的量化器实例化机制（基于E-matching与模型构建）使其也能处理一阶逻辑公式。Z3的TPTP（Thousands of Problems for Theorem Provers）竞赛表现显示，它在"UF（无理论的一阶逻辑）"类别中也具有竞争力。
5 应用领域
5.1 数学定理的形式化验证
5.1.1 四色定理的机器证明
四色定理（任何地图可通过至多四种颜色着色）于1976年由Appel与Haken使用计算机辅助证明，但其部分依赖的手工验证仍存争议。2005年，Georges Gonthier利用Coq对四色定理进行了完全形式化的机器验证，整个过程生成约60,000行Coq代码，并使用了大量图论算法与形状枚举。这一成果展示了ATP在解决"大但结构清晰"的数学问题上的能力。
5.1.2 费马大定理的部分验证
费马大定理的完整证明（由Andrew Wiles完成）极为复杂，至今未被完整形式化。但数学研究者利用ATP系统验证了其中的若干子模块，例如椭圆曲线的模性形式性质、伽罗瓦表示理论中的关键引理等。这些部分验证不仅确保了推理的正确性，也为未来对完整证明进行形式化提供了基石。
5.2 软件与硬件验证
5.2.1 程序终止性与不变式推理
程序的终止性（即程序会有限步结束）是一个不可判定的问题，但ATP系统可自动检查许多经典模式（如循环计数器递减、字典序重写）。通过将程序转换为逻辑公式（如使用分离逻辑或谓词抽象），ATP可自动寻找循环不变式和递归终止条件。例如，ACL2常被用于验证Lisp程序的无终止循环。
5.2.2 微处理器指令集的形式化检查
芯片设计中的一个关键环节是验证指令集架构（ISA）的硬件实现是否正确。此类验证通常将CPU行为建模为一组时态逻辑公式，然后通过ATP/SMT求解器检查实现逻辑是否与规范相符。英特尔、AMD等公司多年来持续使用Vampire、Z3等工具对内部逻辑单元进行形式化验证，从而避免数百万美元的掩膜修正成本。
5.3 人工智能与知识表示
5.3.1 自动问答系统的逻辑推理
知识型问答系统中，常需要将问句转换为逻辑查询，然后从一个公理化的知识库中推理出答案。例如，在CYC（一个大型常识知识库）中，自动定理证明被用于推断："苏格拉底是人且所有人终将死亡"，从而得出"苏格拉底会死"这一结论。这类推理通常使用一阶归结或描述逻辑推理机。
5.3.2 常识推理中的非单调逻辑
真实世界的知识往往具有非单调性：增加新信息可能撤销旧结论（如"鸟一般会飞"与"企鹅不会飞"的冲突）。经典一阶逻辑是单调的，为此产生了缺省逻辑、超循环逻辑等非单调框架。ATP系统在这些框架中的自动化仍处于探索阶段，其难点在于合理处理"例外优先级"和"最小化异常假设"。
6 挑战与未来方向
6.1 搜索空间爆炸与启发式困境
即使使用最先进的删减策略，ATP搜索空间仍然随问题规模呈指数增长。例如，对包含50个公理的特定问题，可能的归结序列数量可达天文数字。传统的启发式（如子句权重、年龄优先级）虽然实用，但缺乏对问题结构的深层理解，导致在不同问题域间的性能波动极大。
6.1.1 随机性与贝叶斯指导的搜索
近年，采用随机化策略（如随机重启、蒙特卡洛树搜索）的ATP系统在某些问题上表现出色。同时，贝叶斯优化被用于自动选择策略参数（如迭代深度上限、权重系数）。更前沿的研究尝试将证明历史构建为马尔可夫决策过程，并用强化学习训练"策略选择网络"，从而动态调整搜索方向。
6.2 高阶与模态逻辑的自动化
当前一阶ATP已相当成熟，但大量数学和哲学问题（如范畴论、模态逻辑、直觉主义逻辑）的自动化推理仍然困难重重。
6.2.1 依赖类型与同伦类型论带来的复杂性
依赖类型（如Coq的CalC of Constructions）允许类型依赖于项的值（如"长度为n的向量"类型），这让数学表述极其精确，但也使得自动化推理面临更复杂的统一问题与归纳模式。同伦类型论（HoTT）进一步引入了"等价"和"高阶路径"概念，使其证明所需的全机械化版本在实用上的自动化程度仍然非常有限。如何将一阶ATP的成熟技术（如归结）有效扩展到这些框架中，是当前理论计算机科学的焦点之一。
6.3 可解释性与协同工作
ATP系统经常产生冗长且难以理解的证明（尤其是归结式证明），这让人类数学家难以检查或从中获取洞察。
6.3.1 ATP输出证明的翻译与可视化
针对此问题，研究者开发了证明翻译器，将机器的逻辑证明转化为更容易阅读的表述。例如，Isabelle的Sledgehammer可从ATP输出中提取关键化简步骤，并标注出所使用的公理。图形化的证明树展示（如使用Turtle图表或交互式HTML）也被引入，帮助用户快速把握证明的宏观结构。
6.3.2 人机协作证明的范式
未来的定理证明可能不是"全自动"或"全手动"的二分法，而是一种人机协作的渐进过程。例如，自动定理证明器可以作为"局部推理引擎"，处理冗长的代数化简或子目标验证；人类数学家则负责顶层策略设计和对核心概念的理解。这种协作已在四色定理、开普勒猜想的形式化中展示了潜力，并且随着交互式证明助手与ATP系统的深度融合，预计将成为数学研究的新常态。