自动定理证明

文档概述

自动定理证明（Automated Theorem Proving, ATP）是人工智能与数理逻辑的交叉领域，旨在设计能在计算机上自动证明数学定理的程序。本文系统阐述归结原理、链接策略、霍恩子句及主流定理证明器，为构建智能推理系统提供方法论基础。

关键词速览

关键词	英文术语	核心含义
归结原理	Resolution	一阶逻辑的完备证明规则
合一	Unification	求取使两个公式相同的替换
子句	Clause	文字的析取式
霍恩子句	Horn Clause	至多一个正文字的子句
前向链接	Forward Chaining	从事实推导结论
后向链接	Backward Chaining	从目标回溯证明
SLD归结	SLD-Resolution	用于逻辑程序的归结
模型检测	Model Checking	有穷状态系统的自动化验证
证明助手	Proof Assistant	交互式定理证明工具

一、自动定理证明概述

1.1 历史沿革

自动定理证明的发展经历了以下阶段：

时期	里程碑事件	代表系统
1950s	逻辑机器	Newell-Shaw-Simon (1956)
1960s	归结原理	Robinson (1965)
1970s	霍恩子句与Prolog	Colmerauer (1972)
1980s	有限模型检测	模型检测工具诞生
1990s	证明助手成熟	Coq, Isabelle
2000s+	深度学习+ATP	AlphaProof等

1.2 问题分类

可判定的证明问题：

命题逻辑的可满足性（SAT）— NP完全
某些一阶理论的可判定片段

不可判定的证明问题：

一般一阶逻辑 — 图灵可识别但不可判定
Peano算术 — 半可判定（完备证明系统存在）

哥德尔不完备性的影响

任何足够强的递归可枚举理论都是不完备的，意味着存在真但不可证明的命题。这限制了自动定理证明的能力边界。

二、归结原理

2.1 子句形式

归结原理作用于子句（clause）——文字的析取式。

定义（文字）：

正文字：原子公式 $P (t_{1}, \dots, t_{n})$
负文字：原子公式的否定 $\neg P (t_{1}, \dots, t_{n})$

定义（子句）：子句是文字的有限集合 ${L_{1}, L_{2}, \dots, L_{n}}$ ，解释为析取 $L_{1} \lor L_{2} \lor \dots \lor L_{n}$ 。

2.2 归结规则

定义（归结规则，Resolution）：

给定两个子句： $C_{1} = L_{1} \lor C_{1}^{'}$ $C_{2} = \neg L_{2} \lor C_{2}^{'}$

若 $L_{1}$ 与 $L_{2}$ 可合一（存在合一子 $θ$ ），则可归结出：

$Res (C_{1}, C_{2}) = (C_{1}^{'} θ) \lor (C_{2}^{'} θ)$

示例：

子句1: P(x) ∨ Q(x)
子句2: ¬P(f(y)) ∨ R(y)
归结: Q(f(y)) ∨ R(y)    （合一子: {x/f(y)}）

2.3 归结反驳证明

策略：要证明 $Γ ⊨ φ$ ，采用反证法：

将 $\neg φ$ 加入前提 $Γ$
将所有公式转化为子句形式
对子句集应用归结规则
若能归结出空子句 $□$ ，则 $Γ ⊨ φ$

空子句的含义

空子句 $□$ 表示矛盾。当归结过程中导出空子句时，意味着前提集与 $\neg φ$ 不一致，因此 $φ$ 必然成立。

2.4 归结的完备性

定理（归结完备性）：

若子句集 $S$ 不可满足，则存在从 $S$ 到空子句的归结证明。

Herbrand定理：

$S$ 不可满足当且仅当存在 $S$ 的有限基例不可满足。

三、链接策略

3.1 前向链接（Forward Chaining）

定义：

前向链接从已知事实出发，应用产生式规则生成新事实，直到达到目标或无法继续。

控制策略：

冲突解决：当多条规则匹配时，选择其一执行
数据驱动：从初始事实向目标状态推理

示例（产生式系统）：

规则1: IF 鸟类(x) ∧ ¬异常(x) THEN 会飞(x)
规则2: IF 会飞(x) THEN 天空生物(x)
事实: 鸟类(麻雀), ¬异常(麻雀)
推导: 会飞(麻雀), 天空生物(麻雀)

复杂度：在最坏情况下为指数级，但实际应用中常有效控制。

3.2 后向链接（Backward Chaining）

定义：

后向链接从目标出发，递归地证明子目标，直到所有子目标都能由已知事实直接满足。

控制策略：

目标驱动：从查询向事实推理
深度优先：递归探索子目标

示例（Prolog查询）：

会飞(x) :- 鸟类(x), 非异常(x).
非异常(x) :- 非受伤(x).
?- 会飞(麻雀).

3.3 混合策略

双向链接：

从已知事实前向传播
从目标后向传播
在中间相遇时完成证明

黑板体系结构：

多个知识源独立工作
通过共享黑板交换信息
协调器管理推理进程

四、霍恩子句与逻辑编程

4.1 霍恩子句的定义

定义（霍恩子句）：

霍恩子句是至多含有一个正文字的子句，形式为： $A \leftarrow B_{1}, B_{2}, \dots, B_{n}$ 或等价地： $\neg B_{1} \lor \neg B_{2} \lor \dots \lor \neg B_{n} \lor A$

分类：

确定性规则：有正文字和负文字
事实：仅含正文字（ $n = 0$ ）
查询：仅含负文字（无正文字）

4.2 SLD归结

定义（SLD归结）：

SLD（Linear resolution with Selection function for Definite clauses）是用于确定子句的线性归结。

SLD反驳过程：

从查询（目标的否定）开始
选择子目标，与规则头合一
递归归结
若空子句出现，则查询成立

4.3 Prolog的推理机制

Prolog执行模型：

% 知识库
parent(tom, bob).
parent(bob, ann).
 
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
 
% 查询
?- ancestor(tom, ann).

搜索策略：

深度优先：Prolog默认
回溯：当分支失败时返回探索其他选择
剪枝：通过cut (!) 控制搜索

Prolog的局限性

深度优先+回溯可能导致：

无限循环（递归定义无终止条件）

非完备性（可能错过解）

顺序敏感性（规则顺序影响结果）

4.4 否定即失败

闭世界假设（CWA）： $\neg P ⟺ 已知 P 为假$

否定即失败（NAF）： $若 P 无法推导，则 \neg P 成立$

失败即否定的问题：

在有穷论域上不完备
可能与默认推理冲突

五、定理证明器

5.1 证明助手的类型

类型	代表系统	特点
交互式	Coq, Isabelle, Lean	人机协作，高可信
自动式	E, Vampire, Z3	完全自动，能力有限
混合式	Mizar	结合自动与手工

5.2 Coq系统

Coq起源：基于直觉类型论与归纳构造

核心概念：

命题即类型： $\Prop$ 是命题的 universes
证明即程序：证明对象是类型 inhabitant
依赖类型：类型依赖于值

示例：

Theorem plus_comm:
  forall n m : nat, n + m = m + n.
Proof.
  induction n.
  - simpl. reflexivity.
  - intros m. simpl. rewrite IHn. reflexivity.
Qed.

应用领域：

四色定理（1998）
奇书之恋定理（2004）
CompCert编译器验证

5.3 Isabelle系统

Isabelle架构：

Pure：纯函数式框架
Isar：结构化证明语言
代发：支持多种逻辑（HOL, ZF, NAT）

证明风格：

lemma "A ⟶ A ∨ B"
proof (rule impI)
  assume A
  show "A ∨ B" by (rule disjI1)
qed

5.4 自动定理证明器

Vampire：

一阶逻辑的自动定理证明
支持丰富的一阶理论（数组、位向量）
多次获CADE ATP系统竞赛冠军

E定理证明器：

基于重写与归结
支持SMT风格的理论
开源实现

Z3：

微软研究院开发
SMT求解器（非纯ATP）
强大的理论求解能力

六、归结策略与优化

6.1 支撑集策略

定义：每次归结，至少有一个亲本子句来自假设集（而非归结过程的产物）。

优点：避免平凡的自我归结，提高效率。

6.2 单元归结优先

策略：优先选择包含单文字（单元子句）的亲本进行归结。

效果：加速矛盾发现，特别适用于有单元公理的理论。

6.3 语义归结

思想：给子句赋予语义值（真/假），只对语义相异的子句归结。

6.4 归结树与限制

策略	描述	完备性
输入归结	至少一个亲本来自输入子句集	不完备
线性归结	亲本之一是前一步的归结结果	完备
单位归结	至少一个亲本是单元子句	不完备
支持集	归结受限于假设集	完备

七、模型检测

7.1 有穷状态模型检测

定义：给定有限状态系统 $M$ 和规格 $φ$ ，检查 $M ⊨ φ$ 。

算法：

状态空间穷举
标注满足 $\neg φ$ 的状态
固定点计算
检查初始状态是否被标注

7.2 CTL模型检测

时序逻辑规格：使用计算树逻辑（CTL）描述系统性质

示例： $A G (req \to A F ack) ：每次请求最终都被确认$

7.3 BDD基础模型检测

有序二元决策图（OBDD）：

表示布尔函数的数据结构
符号化模型检测
避免状态爆炸

八、应用领域

8.1 硬件验证

微处理器设计验证
协议正确性证明
安全协议分析

8.2 软件验证

编译器验证（CompCert）
操作系统验证（seL4）
智能合约验证

8.3 数学证明

四色定理（1976，辅助证明）
Kepler猜想（1998，形式验证）
奇书之恋定理（2004）

8.4 AI推理

知识库问答
自动规划
形式化知识表示验证

参考文献

Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. JACM, 12(1), 23-41.
Lloyd, J. W. (1987). Foundations of Logic Programming (2nd ed.). Springer.
Fitting, M. (2012). Types, Tableaus, and Gödel’s God. Springer.
Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer.
Baader, F., & Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.

人工智能知识库

探索

自动定理证明

自动定理证明

关键词速览

一、自动定理证明概述

1.1 历史沿革

1.2 问题分类

二、归结原理

2.1 子句形式

2.2 归结规则

2.3 归结反驳证明

2.4 归结的完备性

三、链接策略

3.1 前向链接（Forward Chaining）

3.2 后向链接（Backward Chaining）

3.3 混合策略

四、霍恩子句与逻辑编程

4.1 霍恩子句的定义

4.2 SLD归结

4.3 Prolog的推理机制

4.4 否定即失败

五、定理证明器

5.1 证明助手的类型

5.2 Coq系统

5.3 Isabelle系统

5.4 自动定理证明器

六、归结策略与优化

6.1 支撑集策略

6.2 单元归结优先

6.3 语义归结

6.4 归结树与限制

七、模型检测

7.1 有穷状态模型检测

7.2 CTL模型检测

7.3 BDD基础模型检测

八、应用领域

8.1 硬件验证

8.2 软件验证

8.3 数学证明

8.4 AI推理

参考文献

相关文档

关系图谱

目录

反向链接