第09章 一阶逻辑推理

摘要：本章系统阐述一阶逻辑（FOL）推理的核心理论与算法，核心思想是提升（lifting）——通过合一（unification）在变量层面执行推理，避免命题化带来的组合爆炸。主要内容包括：（1）基础概念：替换、全称/存在实例化、命题化与Herbrand定理；（2）核心算法：合一算法、前向链接（数据驱动）、后向链接（目标驱动）及归结（反演完备）；（3）效率优化：Rete网络、表格逻辑编程、归结策略；（4）延伸讨论：合一与注意力机制对比、神经引导定理证明、AI对齐中不可判定性的启示。关键结论：FOL推理是半可判定的，需在表达力、完备性、效率间权衡；Datalog（无函数符号的定子句）落在工业应用的"甜点"上。

对应 Artificial Intelligence: A Modern Approach, 4th Edition 第 9 章 Inference in First-Order Logic

---

1. 章节概述

第 8 章解决了"怎么说"——一阶逻辑（FOL）提供了描述对象、关系、函数与量化断言的语言。本章解决"怎么算"——如何从 FOL 知识库中高效地推导结论。

朴素的思路是把 FOL 归约为命题逻辑：既然 $\forall xP(x)$ 语义上等价于对论域中每个对象的合取，那就把所有变量替换成所有可能的常量，得到一个（可能巨大的）命题逻辑 KB，再用第 7 章的 DPLL/归结求解。这条路线理论上可行（Herbrand 定理保证了它的完备性），但实践中灾难性地低效：$k$ 元谓词、$n$ 个常量会产生 $n^k$ 个命题符号；有函数符号时项集甚至无限。

本章的核心贡献是 提升（lifting） 思想：

不要把变量实例化成所有可能的常量，而是只在必要时、只做必要的替换——这正是 合一（unification） 算法的作用。带合一的推理规则（lifted inference rules）在变量层面一步完成命题层面需要 $n^k$ 步的工作。

本章主线：

1. 命题化（propositionalization）与 Herbrand 定理：理论桥梁，说明 FOL 推理"可以"归约为命题推理。
2. 量词消去：全称实例化（UI）、存在实例化（EI）、Skolem 化。
3. 合一（unification）：FOL 推理的引擎，求最一般合一子（MGU）。
4. 提升的推理规则：广义 Modus Ponens（GMP）。
5. 前向链接（forward chaining）：Datalog、模式匹配、增量式、Rete 网络。
6. 后向链接（backward chaining）：Prolog、SLD 消解、答案抽取。
7. 归结（resolution）：CNF 转换、Skolem 化、二元归结、因子化、完备性证明梗概、实用策略。
8. 逻辑程序设计与定理证明器的工程实践。

读者应带走的核心直觉：

合一是"让两个表达式长得一样"的最小努力；提升是"用一个变量层面的推理步，代替指数多个常量层面的推理步"。所有高效 FOL 推理的秘密都在这两句话里。

---

2. 关键概念与定义

2.1 替换（Substitution）

替换是变量到项的映射，写作 θ={v1/t1,v2/t2,… }\theta = \{v_1/t_1, v_2/t_2, \dots\}θ={v1​/t1​,v2​/t2​,…}。

• $SUBST(\theta ,\alpha )$ 表示把 $\theta$ 应用到句子 $\alpha$ 上的结果。
• 例：SUBST({x/Sam}, Likes(x,IceCream))=Likes(Sam,IceCream)SUBST(\{x/Sam\},\ Likes(x, IceCream)) = Likes(Sam, IceCream)SUBST({x/Sam}, Likes(x,IceCream))=Likes(Sam,IceCream)

术语：

• 基项（ground term）：不含变量的项，如 $Father(John)$。
• 基句子 / 基原子（ground sentence / ground atom）：不含变量的句子。
• 实例化（instantiation）：用替换消去变量的过程。
• 更一般 / 更特殊：若 ${\theta }_1$ 的结果可通过再施加某替换得到 ${\theta }_2$ 的结果，则 ${\theta }_1$ 更一般。

2.2 全称实例化（Universal Instantiation, UI）

∀v  αSUBST({v/g}, α)g 为任意基项\frac{\forall v\ \ \alpha}{SUBST(\{v/g\},\ \alpha)}\qquad g \text{ 为任意基项}SUBST({v/g}, α)∀v  α​g 为任意基项

从"所有国王且贪婪者皆恶":

$$\forall xKing(x)\wedge Greedy(x)\Rightarrow Evil(x)$$

可实例化出无穷多句子：

$$\begin{array}{rl}& King(John)\wedge Greedy(John)\Rightarrow Evil(John)\\ & King(Richard)\wedge Greedy(Richard)\Rightarrow Evil(Richard)\\ & King(Father(John))\wedge Greedy(Father(John))\Rightarrow Evil(Father(John))\\ & \cdots \end{array}$$

⚠️ UI 可应用任意多次，原句子保留在 KB 中。

2.3 存在实例化（Existential Instantiation, EI）

∃v  αSUBST({v/k}, α)k 为 KB 中未出现过的新常量\frac{\exists v\ \ \alpha}{SUBST(\{v/k\},\ \alpha)}\qquad k \text{ 为 KB 中未出现过的新常量}SUBST({v/k}, α)∃v  α​k 为 KB 中未出现过的新常量

$k$ 称为 Skolem 常量（Skolem constant）。

例：$\exists xCrown(x)\wedge OnHead(x,John)$ 可推出

$$Crown(C_1)\wedge OnHead(C_1,John)$$

只要 $C_1$ 是全新符号。

UI 与 EI 的关键差别：

	UI	EI
可应用次数	任意多次	仅一次（用完丢弃原句）
结果与原句关系	逻辑等价（原句蕴涵结果）	推理等价（inferentially equivalent）：新 KB 可满足 iff 原 KB 可满足
新符号	不引入	引入 Skolem 常量

为什么 EI 只能用一次：$\exists xP(x)$ 只保证"至少有一个"，若用两次引入 $C_1,C_2$，就错误地断言了"至少两个"。

为什么 Skolem 常量必须是新的：若复用已有常量 $John$，则等于额外断言"那个满足 $P$ 的对象就是 John"，这是原句没有的信息。

2.4 命题化与 Herbrand 定理

命题化（propositionalization）：把 FOL KB 中所有量化句用 UI/EI 展开为基句子，再把每个基原子（如 $King(John)$）当作一个命题符号，从而得到一个命题逻辑 KB。

问题：若 KB 含函数符号，基项集合是无限的：
$$John,Father(John),Father(Father(John)),\dots$$

Herbrand 定理（Herbrand, 1930）：

若一个句子 $\alpha$ 被 FOL 知识库 $KB$ 蕴涵，则存在 $KB$ 的有限基句子子集蕴涵 $\alpha$。

Herbrand 论域（Herbrand universe）：由 KB 中的常量与函数符号能构造出的所有基项的集合。
Herbrand 基（Herbrand base）：所有基原子的集合。

由 Herbrand 定理导出的算法（半可判定过程）：

for n = 0, 1, 2, ... do
    生成深度 ≤ n 的所有基项
    构造对应的命题化 KB
    用命题推理（DPLL/归结）检查是否蕴涵 α
    if 蕴涵 then return true

• 完备性：若 $KB\models \alpha$，某个有限 $n$ 必然成功。
• 不可判定性体现：若 $KB/\models \alpha$，循环永不终止。

Turing (1936) 与 Church (1936)：FOL 蕴涵是半可判定的（semi-decidable）——存在算法证明蕴涵，但不存在算法在不蕴涵时总能报告"否"。

命题化的两大低效：

1. 无关实例化：为回答 $Evil(John)$，生成了 $Evil(Richard)$、$Evil(Father(John))$ 等无用句子。
2. 组合爆炸：$p$ 个 $k$ 元谓词 + $n$ 个常量 ⇒ $p\cdot n^k$ 个命题符号。

⇒ 需要 lifting。

2.5 合一（Unification）

定义：合一是找一个替换 $\theta$，使两个（或多个）逻辑表达式语法上完全相同：

$$UNIFY(p,q)=\theta \text{使得}SUBST(\theta ,p)=SUBST(\theta ,q)$$

$\theta$ 称为合一子（unifier）。

示例（设 KB 含 $Knows(John,x)$）：

$p$	$q$	$\theta =UNIFY(p,q)$
$Knows(John,x)$	$Knows(John,Jane)$	{x/Jane}\{x/Jane\}{x/Jane}
$Knows(John,x)$	$Knows(y,Bill)$	{x/Bill, y/John}\{x/Bill,\ y/John\}{x/Bill, y/John}
$Knows(John,x)$	$Knows(y,Mother(y))$	{y/John, x/Mother(John)}\{y/John,\ x/Mother(John)\}{y/John, x/Mother(John)}
$Knows(John,x)$	$Knows(x,Elizabeth)$	fail

最后一例失败的原因：同一个变量名 $x$ 在两句中指代不同事物。解决办法是 标准化分离（standardizing apart）：把其中一句的变量重命名，如 $Knows(x_{17},Elizabeth)$，则可合一 {x/Elizabeth, x17/John}\{x/Elizabeth,\ x_{17}/John\}{x/Elizabeth, x17​/John}。

最一般合一子（Most General Unifier, MGU）：

多个合一子可能存在。$UNIFY(Knows(John,x),Knows(y,z))$ 可得：

• θ1={y/John, x/z}\theta_1 = \{y/John,\ x/z\}θ1​={y/John, x/z} ← MGU
• θ2={y/John, x/John, z/John}\theta_2 = \{y/John,\ x/John,\ z/John\}θ2​={y/John, x/John, z/John} ← 更特殊

MGU 对变量施加的约束最少，其他所有合一子都是 MGU 的实例。MGU 在变量换名意义下唯一。

2.6 广义 Modus Ponens（Generalized Modus Ponens, GMP）

$$\frac{p_1^{\prime },p_2^{\prime },\dots ,p_n^{\prime },(p_1\wedge p_2\wedge \cdots \wedge p_n\Rightarrow q)}{SUBST(\theta ,q)}$$

其中存在 $\theta$ 使得对所有 $i$：$SUBST(\theta ,p_i^{\prime })=SUBST(\theta ,p_i)$。

示例：

• $p_1^{\prime }=King(John)$，$p_1=King(x)$
• $p_2^{\prime }=Greedy(y)$，$p_2=Greedy(x)$
• 规则：$King(x)\wedge Greedy(x)\Rightarrow Evil(x)$
• θ={x/John, y/John}\theta = \{x/John,\ y/John\}θ={x/John, y/John}
• 结论：$Evil(John)$

GMP 是提升版（lifted）的 Modus Ponens：一步完成命题版需要先用 UI 枚举再匹配的工作。

可靠性证明：由 UI，$\forall x(p_1\wedge \cdots \wedge p_n\Rightarrow q)\models SUBST(\theta ,p_1\wedge \cdots \wedge p_n\Rightarrow q)$；由前提 $p_i^{\prime }$ 与 $SUBST(\theta ,p_i^{\prime })=SUBST(\theta ,p_i)$，命题版 Modus Ponens 给出 $SUBST(\theta ,q)$。∎

2.7 一阶定子句与 Datalog

• 一阶定子句（first-order definite clause）：形如 $p_1\wedge \cdots \wedge p_n\Rightarrow q$ 的蕴涵式，其中所有 $p_i$、$q$ 是正原子；变量隐含全称量化。原子事实（$n=0$）也算。
• Datalog：无函数符号的一阶定子句语言。
  • 关键性质：Herbrand 论域有限（只有常量），因此推理可判定。
  • 广泛用于演绎数据库、图查询、程序分析。

⚠️ 有函数符号的定子句（如 Prolog）失去可判定性——因为可以生成无限多项。

---

3. 核心理论与算法

3.1 合一算法（UNIFY）

function UNIFY(x, y, θ=empty) returns 一个替换，使 x 与 y 相同，或 failure
    inputs: x, y —— 变量、常量、列表或复合表达式
            θ   —— 到目前为止建立的替换（默认为空）

    if θ = failure then return failure
    else if x = y then return θ
    else if VARIABLE?(x) then return UNIFY-VAR(x, y, θ)
    else if VARIABLE?(y) then return UNIFY-VAR(y, x, θ)
    else if COMPOUND?(x) and COMPOUND?(y) then
        return UNIFY(x.ARGS, y.ARGS, UNIFY(x.OP, y.OP, θ))
    else if LIST?(x) and LIST?(y) then
        return UNIFY(x.REST, y.REST, UNIFY(x.FIRST, y.FIRST, θ))
    else return failure


function UNIFY-VAR(var, x, θ) returns 一个替换
    if {var/val} ∈ θ for some val then return UNIFY(val, x, θ)
    else if {x/val}  ∈ θ for some val then return UNIFY(var, val, θ)
    else if OCCUR-CHECK?(var, x) then return failure
    else return add {var/x} to θ

逐行解读：

1. 递归结构：从表达式外层向内层递归，逐对比较对应位置。
2. 变量绑定：遇到变量就尝试绑定；若变量已有绑定，递归合一其绑定值。
3. OCCUR-CHECK（出现检验）：检查 $var$ 是否出现在 $x$ 内部。若 $UNIFY(x,f(x))$ 不做检验，会产生无限项 $f(f(f(\dots )))$。

• 代价：朴素实现使合一从 $O(size)$ 变为 $O(n^2)$。
• Prolog 的选择：默认省略 occur-check，因此 Prolog 的推理不可靠（unsound）——但在实践中极少出问题，换来了显著的速度。这是工程与理论的经典权衡。

4. 复杂度：朴素实现 $O(n^2)$；使用结构共享（structure sharing）与并查集的算法可达 线性时间 $O(n)$（Martelli–Montanari 算法、Paterson–Wegman 算法）。

MGU 保证：该算法返回的合一子总是最一般的——因为它只在必要时绑定变量，且优先绑定变量到变量。

关键设计要点：标准化分离（standardizing apart）
每次使用 KB 中的规则前，必须把规则中的变量重命名为全新变量。否则不同规则实例间会发生变量名冲突，导致错误的失败或过度约束。

3.2 前向链接（Forward Chaining）

3.2.1 一阶定子句的前向链接算法

function FOL-FC-ASK(KB, α) returns 一个替换或 false
    inputs: KB —— 一阶定子句知识库
            α  —— 查询（原子句子）

    while true do
        new ← {}                     // 本轮新推出的句子
        for each rule in KB do
            (p₁ ∧ ... ∧ pₙ ⇒ q) ← STANDARDIZE-VARIABLES(rule)
            for each θ such that SUBST(θ, p₁ ∧ ... ∧ pₙ)
                                = SUBST(θ, p₁' ∧ ... ∧ pₙ')
                for some p₁',...,pₙ' in KB do
                    q' ← SUBST(θ, q)
                    if q' 不与 KB 或 new 中已有句子 unify then
                        add q' to new
                        φ ← UNIFY(q', α)
                        if φ is not failure then return φ
        if new = {} then return false
        add new to KB

经典示例（“West 是罪犯”）：

KB：
$$\begin{array}{rl}& \text{R1: }American(x)\wedge Weapon(y)\wedge Sells(x,y,z)\wedge Hostile(z)\Rightarrow Criminal(x)\\ & \text{R2: }Missile(x)\wedge Owns(Nono,x)\Rightarrow Sells(West,x,Nono)\\ & \text{R3: }Missile(x)\Rightarrow Weapon(x)\\ & \text{R4: }Enemy(x,America)\Rightarrow Hostile(x)\\ & \text{F1: }Owns(Nono,M_1)\text{F2: }Missile(M_1)\\ & \text{F3: }American(West)\text{F4: }Enemy(Nono,America)\end{array}$$

推理过程：

第 1 轮：
  R3 + F2 → Weapon(M₁)
  R2 + F2,F1 → Sells(West, M₁, Nono)
  R4 + F4 → Hostile(Nono)
第 2 轮：
  R1 + F3, Weapon(M₁), Sells(West,M₁,Nono), Hostile(Nono)
     → Criminal(West)   ✓

⚠️ 注意 $\exists x\dots$ 形式的存在句在此前需先 Skolem 化，$Owns(Nono,M_1)$ 中的 $M_1$ 即 Skolem 常量。

3.2.2 性质分析

性质	说明
可靠性	GMP 可靠 ⇒ 前向链接可靠
完备性	对一阶定子句 KB 完备（证明用 Herbrand 模型构造）
终止性	Datalog（无函数符号）：必然终止，最多 $p\cdot n^k$ 个基事实 有函数符号：可能不终止（如 $NatNum(x)\Rightarrow NatNum(S(x))$ 无限生成）
复杂度	Datalog：$O(p\cdot n^k)$ 个可能事实，判定蕴涵是 数据复杂度 P-完全、组合复杂度 EXPTIME

3.2.3 三大效率问题与对策

问题 1：模式匹配代价高（Matching）

在每轮中为规则找到所有满足的 $\theta$，本质是一个 约束满足问题（CSP）。例如：

$$Missile(x)\wedge Owns(Nono,x)\Rightarrow \dots$$

要在成千上万事实中找所有匹配。结论：规则匹配等价于 CSP，因此是 NP-难 的（一般情形）。

对策：

• CSP 技术：变量排序（最受约束优先）、弧相容。
• 合取序优化：先匹配约束最强的合取项（如 $Owns(Nono,x)$ 通常比 $Missile(x)$ 更具选择性）——这是 conjunct ordering 问题，本身 NP-难，用启发式（最小剩余值 MRV）。
• 数据索引：为谓词建立哈希表/多路索引（如按谓词名+参数位置建 index），使检索 $O(1)$。

问题 2：重复推理（Incremental Forward Chaining）

朴素算法每轮重推所有规则，重复大量工作。

关键洞察：

第 $t$ 轮推出的每个新事实，必然使用了第 $t-1$ 轮新推出的某个事实。

增量式前向链接：只对至少匹配一个"上一轮新事实"的规则做匹配。

Rete 算法（Forgy, 1982）：

• 把所有规则的前提编译成一个共享的数据流网络（dataflow network）。
• 公共子表达式在网络中共享节点，避免重复计算。
• 事实的增删只沿网络传播增量。
• 是生产系统（production system）如 OPS-5、CLIPS、Jess、Drools 的核心，也是许多规则引擎、XCON 专家系统的基础。

问题 3：无关事实（Irrelevant Facts）

前向链接会推出大量与查询无关的结论。

对策：

• 魔集变换（magic sets）：一种规则重写技术，把后向链接的目标导向性"编译进"前向链接规则。通过给规则加上"magic 谓词"作为额外前提，限制只推理与查询相关的实例。这是演绎数据库领域的标准优化。
• 直接改用后向链接。

适用场景总结：

• ✓ 事实增量到达、需推出全部结论（监控系统、实时规则引擎、演绎数据库物化视图）。
• ✗ 目标明确且 KB 巨大（应改用后向链接）。

3.3 后向链接（Backward Chaining）

3.3.1 算法

function FOL-BC-ASK(KB, query) returns 替换的生成器
    return FOL-BC-OR(KB, query, { })

function FOL-BC-OR(KB, goal, θ) returns 替换
    for each rule (lhs ⇒ rhs) in FETCH-RULES-FOR-GOAL(KB, goal) do
        (lhs, rhs) ← STANDARDIZE-VARIABLES((lhs, rhs))
        for each θ' in FOL-BC-AND(KB, lhs, UNIFY(rhs, goal, θ)) do
            yield θ'

function FOL-BC-AND(KB, goals, θ) returns 替换
    if θ = failure then return
    else if LENGTH(goals) = 0 then yield θ
    else
        first, rest ← FIRST(goals), REST(goals)
        for each θ' in FOL-BC-OR(KB, SUBST(θ, first), θ) do
            for each θ'' in FOL-BC-AND(KB, rest, θ') do
                yield θ''

结构解读：

• AND-OR 树：一条规则的多个前提是 AND 分支（都要证明）；同一目标的多条规则是 OR 分支（任一成功即可）。
• 生成器（generator）：返回替换流，支持"要一个解就停"或"要全部解"。
• 深度优先 + 回溯：空间复杂度线性于证明深度，但不完备（可能陷入无限循环）。

证明树示例（$Criminal(West)$）：

Criminal(West)
 └─ 用 R1，θ = {x/West}
    ├─ American(West)                    ✓ (F3)
    ├─ Weapon(y)
    │   └─ 用 R3，θ = {y/M₁}
    │       └─ Missile(M₁)               ✓ (F2)
    ├─ Sells(West, M₁, z)
    │   └─ 用 R2，θ = {z/Nono}
    │       ├─ Missile(M₁)               ✓ (F2)
    │       └─ Owns(Nono, M₁)            ✓ (F1)
    └─ Hostile(Nono)
        └─ 用 R4
            └─ Enemy(Nono, America)      ✓ (F4)

3.3.2 逻辑程序设计（Prolog）

Prolog 是后向链接的工业实现，语法特点：

• 大写为变量，小写为常量：criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z).
• 规则按书写顺序尝试，前提按从左到右求解 ⇒ 深度优先、从左到右的搜索策略。

Prolog 的关键工程决策与代价：

决策	收益	代价
深度优先搜索	空间 $O(depth)$，速度快	不完备：左递归规则 path(X,Y) :- path(X,Z), edge(Z,Y). 无限循环
省略 occur-check	合一 $O(n)$	推理不可靠（unsound）
封闭世界 + 否定即失败（NAF）	高效表示"不成立"	非单调，与经典逻辑语义不同
cut（!）	剪枝控制，提升效率	破坏声明式语义，程序难以理解

否定即失败（Negation as Failure）：\+ P 意为"P 无法被证明"，而非"P 为假"。这是非单调推理：加入新事实可能推翻旧结论。它对应封闭世界假设。

关键优化技术：

• 编译到 WAM（Warren Abstract Machine）：把 Prolog 程序编译成抽象机指令，比解释执行快数量级。
• 开放列表 / 差分表（open list, difference list）：实现 $O(1)$ 的列表拼接。
• OR-并行 与 AND-并行：多个规则/多个前提并行求解。

3.3.3 冗余与记忆化：表格逻辑编程

问题：后向链接会重复求解相同子目标。斐波那契式重复导致指数爆炸。

表格逻辑编程（tabled logic programming / SLG resolution）：

• 用记忆化（memoization）缓存子目标的解。
• 效果：把指数复杂度降为多项式；保证 Datalog 程序终止且完备。
• 实现：XSB Prolog、SWI-Prolog 的 :- table 指令。
• 本质：动态规划 + 后向链接，与前向链接的完备性对齐。

3.4 归结（Resolution）—— 提升版

3.4.1 FOL 的 CNF 转换

比命题逻辑多两步：变量标准化与 Skolem 化。

完整步骤（以 $\forall x[\forall yAnimal(y)\Rightarrow Loves(x,y)]\Rightarrow [\exists yLoves(y,x)]$ 为例，“爱所有动物的人会被某人爱”）：

Step 1. 消去 $\iff$ 与 $\Rightarrow$

$$\forall x[\neg \forall y\neg Animal(y)\vee Loves(x,y)]\vee [\exists yLoves(y,x)]$$

Step 2. 否定内移（De Morgan + 量词对偶 $\neg \forall xp\equiv \exists x\neg p$）

$$\begin{array}{rl}& \forall x[\exists y\neg (\neg Animal(y)\vee Loves(x,y))]\vee [\exists yLoves(y,x)]\\ & \forall x[\exists yAnimal(y)\wedge \neg Loves(x,y)]\vee [\exists yLoves(y,x)]\end{array}$$

Step 3. 变量标准化（同名不同辖域的变量重命名）

$$\forall x[\exists yAnimal(y)\wedge \neg Loves(x,y)]\vee [\exists zLoves(z,x)]$$

Step 4. Skolem 化（消去 $\exists$）

⚠️ 这里是难点：$y$ 与 $z$ 都在 $\forall x$ 的辖域内，其取值依赖于 $x$，因此不能用常量，必须用 Skolem 函数：

$$\forall x[Animal(F(x))\wedge \neg Loves(x,F(x))]\vee Loves(G(x),x)$$

Skolem 化通则：

每个存在量化变量替换为一个 Skolem 函数，其参数是所有外层全称量化变量。若无外层 $\forall$，则退化为 Skolem 常量。

$$\forall x_1\dots \forall x_n\exists y\varphi ⇝\forall x_1\dots \forall x_n\varphi [y/f(x_1,\dots ,x_n)]$$

Skolem 化保持可满足性（satisfiability-preserving），不保持逻辑等价。

Step 5. 丢弃全称量词（此时所有变量都是全称量化的，可隐含）

$$[Animal(F(x))\wedge \neg Loves(x,F(x))]\vee Loves(G(x),x)$$

Step 6. 分配 $\vee$ over $\wedge$

$$[Animal(F(x))\vee Loves(G(x),x)]\wedge [\neg Loves(x,F(x))\vee Loves(G(x),x)]$$

得到两个子句。✓

3.4.2 提升的归结规则（Lifted / Binary Resolution）

$$\frac{{\ell }_1\vee \cdots \vee {\ell }_k,m_1\vee \cdots \vee m_n}{SUBST(\theta ,{\ell }_1\vee \cdots {\ell }_{i-1}\vee {\ell }_{i+1}\cdots \vee {\ell }_k\vee m_1\cdots m_{j-1}\vee m_{j+1}\cdots \vee m_n)}$$

其中 $\theta =UNIFY({\ell }_i,\neg m_j)$。

示例：

$$\frac{[Animal(F(x))\vee Loves(G(x),x)],[\neg Loves(u,v)\vee \neg Kills(u,v)]}{[Animal(F(x))\vee \neg Kills(G(x),x)]}$$

用 θ={u/G(x), v/x}\theta = \{u/G(x),\ v/x\}θ={u/G(x), v/x}。

因子化（factoring）：若一个子句中两个文字可合一，须合并。例：$Loves(x,Cat)\vee Loves(John,y)$ 可因子化为 $Loves(John,Cat)$（用 θ={x/John,y/Cat}\theta=\{x/John, y/Cat\}θ={x/John,y/Cat}）。

⚠️ 没有因子化，归结不完备。这是 Robinson 归结的必要组成部分。

3.4.3 归结反演算法

function FOL-RESOLUTION(KB, α) returns true or false
    clauses ← CNF(KB ∧ ¬α)
    new ← {}
    loop do
        for each pair (Ci, Cj) of clauses do
            (Ci, Cj) ← STANDARDIZE-APART(Ci, Cj)
            resolvents ← RESOLVE(Ci, Cj)           // 含 unification + factoring
            if □ ∈ resolvents then return true      // 空子句 ⇒ 矛盾 ⇒ KB ⊨ α
            new ← new ∪ resolvents
        if new ⊆ clauses then return false
        clauses ← clauses ∪ new

“Curiosity killed the cat” 完整证明（书中经典例题）：

前提（自然语言）：

1. 所有爱一切动物的人，都被某人爱。
2. 任何杀死动物的人，不被任何人爱。
3. Jack 爱所有动物。
4. Jack 或 Curiosity 杀死了猫 Tuna。
5. Tuna 是猫。6. 所有猫都是动物。

目标：$Kills(Curiosity,Tuna)$

CNF 子句：

A1. ¬Animal(y) ∨ Loves(F(x), x)   ... [由 1 Skolem 化]
A2. ¬Loves(x, F(x)) ∨ Loves(G(x), x)
B.  ¬Loves(y,x) ∨ ¬Animal(z) ∨ ¬Kills(x,z)
C.  ¬Animal(x) ∨ Loves(Jack, x)
D.  Kills(Jack,Tuna) ∨ Kills(Curiosity,Tuna)
E.  Cat(Tuna)
F.  ¬Cat(x) ∨ Animal(x)
¬G. ¬Kills(Curiosity, Tuna)      [目标否定]

归结链（简述）：

E + F                  → Animal(Tuna)
D + ¬G                 → Kills(Jack, Tuna)
Animal(Tuna) + C       → Loves(Jack, Tuna)  ... 实际需配合 A1/A2
... + B + Kills(Jack,Tuna)  → ¬Loves(y, Jack)     [没人爱 Jack]
A1/A2 + C 归结         → Loves(G(Jack), Jack)     [有人爱 Jack]
两者归结               → □                        ✓

归结产生矛盾，故 $KB\models Kills(Curiosity,Tuna)$。

注意其中的"反证结构"：从否定目标出发，推出"Jack 杀了 Tuna" ⇒ “没人爱 Jack”；但前提 1+3 又推出"有人爱 Jack" ⇒ 矛盾。这是一个人类也需要动脑的推理，展示了归结的威力。

3.4.4 完备性

Gödel 完备性定理（1930）+ Robinson (1965)：

归结对 FOL 是 反演完备的（refutation-complete）：若 $S$ 是不可满足的子句集，则归结必能推出空子句。

证明梗概（三步）：

1. Herbrand 定理：若 $S$ 不可满足，则存在有限的基实例集 $S^{\prime }$ 不可满足。
2. Ground Resolution Theorem（第 7 章）：命题层面的归结对 $S^{\prime }$ 完备，能推出 $\square$。
3. 提升引理（Lifting Lemma）：若基句子层面存在归结证明，则变量层面存在对应的证明，且基证明是提升证明的实例。

$$\frac{C_1,C_2}{C}\text{(ground)}⟹\frac{C_1^{\prime },C_2^{\prime }}{C^{\prime }}\text{(lifted)},C=SUBST(\theta ,C^{\prime })$$

∎

3.4.5 归结策略（Resolution Strategies）

朴素归结的搜索空间呈指数爆炸，实用系统必须用策略：

策略	原理	完备性
单元优先（unit preference）	优先归结含单个文字的子句，快速缩短子句	保持完备（作为排序启发式）
支持集（set of support）	每步至少一个归结项来自"支持集"（通常初始为否定目标及其后代）	若支持集选择恰当（如 KB 本身可满足），保持完备
输入归结（input resolution）	每步至少一个归结项来自原始输入子句	对 Horn 子句完备，一般 FOL 不完备
线性归结（linear resolution）	允许与祖先子句归结	完备（输入归结的完备化）
subsumption（子句包含）	删除被更一般子句蕴涵的特殊子句	保持完备，大幅剪枝
学习 / lemma 复用	缓存已证子目标	类似 tabling

SLD 消解（Selective Linear Definite clause resolution）：

线性归结 + 定子句 + 选择函数 = Prolog 的推理机制。对定子句完备。

其他实用技术：

• 索引（indexing）：predicate indexing、subsumption lattice、discrimination tree 加速子句检索。
• 等词处理：单纯把 $=$ 当普通谓词并加公理（自反、对称、传递、替换）效率极差。实用方案：
  • 解调（demodulation）：用单元等式 $x=y$ 定向重写项。
  • 超调 / 旁路（paramodulation）：更一般的等式归结规则，对带等词的 FOL 完备。
  • 合一模等理论（E-unification）、Knuth–Bendix 完备化：把等式集编译成合流终止的重写系统。

现代定理证明器：Vampire、E、SPASS、Prover9、Z3（SMT）。它们已解决多个开放数学问题（如 Robbins 猜想由 EQP 于 1996 年证明）。

3.5 前向 vs 后向：完备性与效率总结

维度	前向链接	后向链接	归结
输入限制	一阶定子句	一阶定子句	任意 FOL（转 CNF）
驱动方式	数据驱动（bottom-up）	目标驱动（top-down）	反演（refutation）
可靠性	✓	✓（Prolog 因省 occur-check 而不严格可靠）	✓
完备性	✓（对定子句）	✓（若用 BFS/tabling）；Prolog 的 DFS 不完备	✓（反演完备，对全 FOL）
终止性	Datalog ✓；有函数符号 ✗	可能左递归死循环；tabling 可救	半可判定，可能不终止
空间	存储所有推出事实，可能巨大	$O(depth)$，很省	子句集增长，可能巨大
无关推理	严重（可用 magic sets 缓解）	很少（目标导向）	中等（可用 set of support 缓解）
典型系统	CLIPS、Drools、Datalog 引擎、Rete	Prolog、XSB、专家系统	Vampire、E、SPASS
适用场景	事实流式到达、需全部结论、监控	明确查询、诊断问答、逻辑编程	数学定理证明、形式验证、任意 FOL

局限性汇总：

1. 定子句限制：前向/后向链接无法处理析取结论（$P\Rightarrow Q\vee R$）与否定——这正是需要完整归结的原因。
2. 半可判定性：任何完备的 FOL 推理算法在"不蕴涵"时都可能不终止。实用系统必须设资源上限。
3. 等词爆炸：朴素等词公理化使搜索空间急剧膨胀。
4. 命题化不可取：$n^k$ 爆炸，且函数符号导致无限论域。

---

4. 关键图示/表格说明

4.1 合一示例对照表

$p$	$q$	MGU $\theta$	说明
$Knows(John,x)$	$Knows(John,Jane)$	{x/Jane}\{x/Jane\}{x/Jane}	变量绑定到常量
$Knows(John,x)$	$Knows(y,Bill)$	{x/Bill, y/John}\{x/Bill,\ y/John\}{x/Bill, y/John}	双向绑定
$Knows(John,x)$	$Knows(y,Mother(y))$	{y/John, x/Mother(John)}\{y/John,\ x/Mother(John)\}{y/John, x/Mother(John)}	绑定到复合项，需级联
$Knows(John,x)$	$Knows(x,Elizabeth)$	fail	变量名冲突，需标准化分离
$Knows(John,x)$	$Knows(y,z)$	{y/John, x/z}\{y/John,\ x/z\}{y/John, x/z}	MGU（非 {y/John,x/John,z/John}\{y/John,x/John,z/John\}{y/John,x/John,z/John}）
$x$	$f(x)$	fail（occur-check）	无出现检验则产生无限项
$f(a,g(x))$	$f(y,g(b))$	{y/a, x/b}\{y/a,\ x/b\}{y/a, x/b}	结构递归
$f(a)$	$g(a)$	fail	函数符号不同

4.2 UI / EI / Skolem 化对照

原句	处理	结果
$\forall xP(x)$	UI（可多次）	$P(a)$、$P(b)$、$P(f(a))$…
$\exists xP(x)$	EI（一次）	$P(C_1)$，$C_1$ 为新 Skolem 常量
$\forall x\exists yP(x,y)$	Skolem 化	$\forall xP(x,f(x))$，$f$ 为 Skolem 函数
$\exists y\forall xP(x,y)$	Skolem 化	$\forall xP(x,C)$，$C$ 为 Skolem 常量

⚠️ 最后两行的对比极其重要：Skolem 函数的参数正是外层的全称变量，这准确地编码了"$y$ 依赖 $x$"还是"$y$ 不依赖 $x$"。

4.3 证明树（AND-OR 树）示意

后向链接的搜索空间：

                   Criminal(West)          ← 目标
                        │ OR (可用规则)
                    ┌───┴───┐
                   R1      (其他规则)
                    │ AND (所有前提)
    ┌───────┬───────┼──────────┬─────────┐
American  Weapon  Sells      Hostile
(West)     (y)   (West,y,z)   (z)
   │        │ OR     │ OR       │ OR
  ✓ F3     R3       R2         R4
            │ AND    │ AND      │ AND
        Missile(y)  ┌─┴──┐   Enemy(z,America)
            │    Missile  Owns      │
           ✓F2    (y)  (Nono,y)    ✓F4
                   │      │
                  ✓F2    ✓F1

读图要点：

• 圆形分叉 = OR（规则选择），需要任一成功。
• 方形分叉 = AND（前提合取），需要全部成功。
• 叶节点为 KB 中的事实。
• 深度优先遍历此树 + 回溯 = Prolog 执行模型。
• 替换 $\theta$ 沿树向下传播（合成），子目标的解绑定影响兄弟子目标。

4.4 归结证明的"反演"结构

        KB ∧ ¬α  的子句集
              │
        反复归结（unify + factor）
              ↓
        ...新子句...
              ↓
             □（空子句）
              │
      ⇒ KB ∧ ¬α 不可满足
      ⇒ KB ⊨ α                  ✓

对比第 7 章：结构完全相同，唯一差别是每一步归结内嵌了 unification。这正是"提升"的含义。

4.5 复杂度与可判定性总览

语言片段	蕴涵判定	前向链接终止	典型复杂度
命题定子句	可判定	✓	$O(n)$ 线性
Datalog（FOL 定子句，无函数符号）	可判定	✓	数据复杂度 P-完全；组合复杂度 EXPTIME
FOL 定子句（有函数符号，即 Prolog）	半可判定	✗	不可判定
完整 FOL	半可判定	—	不可判定（Church–Turing）
FOL + 等词	半可判定	—	需 paramodulation
描述逻辑 $\mathcal{A}\mathcal{LC}$	可判定	—	PSPACE-完全

核心 takeaway：表达力 ↔ 可判定性/效率是知识表示的永恒权衡。Datalog 之所以在工业界（数据库、程序分析、Souffle、Datomic）广泛应用，正是因为它落在"表达力够用 + 可判定 + 多项式数据复杂度"的甜点上。

4.6 Rete 网络示意（增量前向链接）

事实流 →  [α 节点：单谓词过滤]
             Missile(?x)      Owns(Nono,?y)
                  │                 │
                  └────┬────────────┘
                       ↓
            [β 节点：连接（join），约束 ?x = ?y]
                       ↓
                 [规则激活]
                Sells(West,?x,Nono)

• α 网络：对单个事实做谓词与常量过滤。
• β 网络：做多事实的连接（join），维护部分匹配的中间结果（记忆节点）。
• 事实增加时只沿网络传播增量，事实删除时撤销传播。
• 空间换时间：中间结果占用大量内存，是 Rete 的主要代价。

---

5. 与其他章节的关联

5.1 承前

章节	关联
第 7 章	归结、CNF、定子句、前向/后向链接的命题版本在此全部被"提升"；Ground Resolution Theorem 是本章完备性证明的第 2 步
第 8 章	本章是第 8 章语言的计算实现；UI/EI 直接源自 FOL 的量词语义；Skolem 化处理的正是 $\exists$
第 6 章 CSP	§3.2.3 明确指出规则匹配 = CSP，因此 MRV、弧相容等技术可直接迁移到 conjunct ordering
第 3 章 搜索	后向链接 = AND-OR 图的深度优先搜索；归结 = 子句空间中的搜索，策略即启发式

5.2 启后

章节	关联
第 10 章 知识表示	描述逻辑（description logic）是为了可判定性而设计的 FOL 片段，其推理算法（tableau）与本章思路一脉相承；语义网 OWL 的推理机（Pellet、HermiT）即基于此
第 11 章 规划	规划器的动作实例化（grounding）本质是合一；PDDL 的前提匹配就是 §3.2.3 的模式匹配问题；GraphPlan 的 mutex 传播类似 Rete 的增量传播
第 12 章 机器人 KR	situation calculus 的推理需要处理带 situation 项的合一；event calculus 常用 Prolog + abduction 实现
第 15 章 关系概率模型	lifted inference 的概率版本：lifted variable elimination、lifted belief propagation，思想完全一致——在变量层面而非基实例层面计算
第 19 章 ILP	归纳逻辑编程用 $\theta$-subsumption（基于合一的一般性偏序）组织假设空间；逆归结（inverse resolution）是归结的反向操作

5.3 一条贯穿的技术线：Lifting

命题逻辑推理（第7章）
    │  变量实例化爆炸
    ↓
命题化 + Herbrand 定理（本章 §2.4）—— 理论可行但低效
    │  引入 unification
    ↓
Lifted inference：GMP / lifted resolution（本章）
    │  推广到概率
    ↓
Lifted probabilistic inference（第15章）
    │  推广到学习
    ↓
Inductive Logic Programming（第19章）

---

6. 延伸思考

6.1 合一 vs 注意力：LLM 有"变量绑定"吗？

合一（unification）是本章最核心的机制。它的功能可以概括为：在两个结构化表达式之间建立变量到项的一致映射，且这个映射对整个表达式全局一致。

关键词是"全局一致"：一旦 $x/John$，则表达式中所有 $x$ 都必须是 $John$。这是 Transformer 注意力机制不天然具备的能力。

机制	合一（unification）	注意力（attention）
匹配方式	精确的结构递归匹配	连续的相似度加权
变量绑定	全局一致，硬约束	无显式变量概念
失败处理	明确 fail，触发回溯	软失败，产生低权重（仍输出）
复合项	递归处理任意深度	深度受层数限制
泛化到新常量	完全免费（变量与实例无关）	依赖训练分布

开放性问题 1：

现代 LLM 在解决"链式推理"任务时，是在近似执行合一，还是在做表层模式检索？

一个可判别的实验设计：

• 构造一批 FOL 推理题，其中实体名从未在训练中出现（如 Zorblax、Quinthar）。
• 若模型真的在做变量绑定，性能应与用常见名字（Alice、Bob）时几乎相同。
• 已有研究表明性能确实会下降，暗示模型部分依赖实体的分布式表示而非纯结构。

更深的问题：Transformer 的深度 $L$ 限制了它能执行的串行推理步数（每层大致对应一步"计算"）。而后向链接的证明树深度是无界的。这在理论上给出了一个根本性限制：

固定深度的 Transformer 无法在单次前向传播中完成任意深度的逻辑推理链。CoT 通过把中间结果写进上下文来"外化"工作记忆，等效于把串行深度从 $L$ 扩展到 $L\times T$（$T$ 为生成的 token 数）。

这与本章的 tabling / 记忆化（§3.3.3）思想惊人地相似——都是用外部存储换取推理深度。可以说，CoT 是"神经版的 SLG 消解"：把子目标的中间结论显式写出来，避免重复计算，也突破单次计算的深度上限。

6.2 神经引导的定理证明：把 LLM 当作启发式函数

本章反复出现的瓶颈是搜索空间爆炸：

• 归结要选哪对子句归结？
• 后向链接要先展开哪个子目标？
• 前向链接的 conjunct ordering 怎么排？

这些都是启发式选择问题，而人类数学家的强项恰在于此。

当前进展：

• AlphaGeometry（2024）：LLM 提出辅助构造（“作 $BC$ 的中点 $M$”），符号引擎做演绎闭包。在 IMO 几何题上达到金牌水平。这完美对应本章的分工：LLM ≈ 决定引入哪个 Skolem 项 / 哪条引理；符号引擎 ≈ 可靠完备的归结。
• LeanDojo / DeepSeek-Prover：LLM 生成 Lean 战术（tactic），证明助手验证每一步。验证器保证 soundness，LLM 提供 搜索效率。
• NeuroSAT / GNN for SAT：用图神经网络学习变量选择启发式，替代 VSIDS。

开放性问题 2：

本章的完备性定理（归结反演完备）保证"只要给足时间就能找到证明"。神经引导只改变搜索顺序，不改变可达性。那么，一个"完备性由符号引擎保证、效率由神经网络提供"的混合架构，是否是可信 AI 推理的正确范式？

值得深思的几个层面：

1. 可验证性不对称：证明的生成极难（搜索），验证极易（线性检查每步）。这个不对称性是混合架构成立的基础，也是 AI 安全中"可扩展监督"（scalable oversight）的希望所在——我们不需要理解 AI 如何想到答案，只需要能验证答案。

2. 但不是所有任务都有廉价验证器。数学证明有（Lean/Coq）；代码有（测试/类型系统）；而"这个医疗建议是否恰当"、"这段文本是否有害"没有。本章的方法论只在可形式化的领域直接适用。

3. Prolog 的教训值得警惕：§3.3.2 提到 Prolog 为效率牺牲了 occur-check（不可靠）和完备性（深度优先）。这在实践中"几乎总是没问题"——但"几乎"意味着存在静默失败的可能。今天用 LLM 做推理时，我们做的是更激进的同类权衡：牺牲所有形式保证，换取极大的适用范围。区别在于，Prolog 的不可靠性有精确刻画（我们知道它在什么情况下出错），而 LLM 的失效模式无法刻画。

6.3 Lifted inference 与多模态、可扩展性

lifting 的核心思想——“在抽象层面一次性处理一整类实例”——远超逻辑范畴：

• 概率推理（第 15 章）：lifted variable elimination 处理"1000 万个用户，每个都有相同的概率结构"，不必展开成 1000 万个变量。
• 多模态感知：视频中的 100 个相同行人，是否需要 100 套独立参数？还是应该有一个"行人"的抽象模板 + 个体化的绑定？这正是 object-centric learning（Slot Attention、MONet）的核心问题——在感知层实现"变量与实例的分离"。
• 具身智能：机器人学会"拿起杯子"后，遇到没见过的杯子应该零样本迁移。这要求策略以变量化的方式表示（“拿起 $?x$，其中 $Graspable(?x)$”），而非记忆具体像素。

一个具体的开放问题：

目前的视觉基础模型（SAM、DINO）能分割和识别对象，但不能表达对象间的量化关系（“所有红色方块都在蓝色方块左边”）。要弥合这个鸿沟，是应该在视觉模型之上接一个符号层（做 scene graph → FOL → 推理），还是应该设计天然支持关系与量化的神经架构？

前者可行但脆弱（依赖场景图的质量，误差传播）；后者优雅但至今没有令人信服的方案。这或许是神经-符号研究最有价值的未解问题。

6.4 AI 对齐视角：不可判定性的启示

本章有一个容易被当作"技术细节"忽略、但对 AI 安全极为重要的结论：

FOL 蕴涵是半可判定的。

这意味着：

• 若某条安全性质被违反，理论上可以找到证明（有限步）。
• 若某条安全性质成立，可能永远无法确认。

对形式化 AI 安全的直接后果：

1. 验证不对称：找 bug（找反例）在原理上比证明"没有 bug"更容易。这解释了为什么红队测试（red-teaming）在实践中比形式验证更主流。
2. 必须限制表达力：模型检验（model checking）之所以在硬件验证中成功，是因为它工作在有限状态（可判定）而非 FOL。要对 AI 系统做形式保证，可能必须把安全性质表达在可判定片段（时序逻辑 LTL/CTL、描述逻辑、Datalog）中。
3. 资源界限即安全界限：任何实际的推理系统都有时间上限。当推理器"超时"时，系统应该默认拒绝（fail-safe）还是默认放行（fail-open）？在 Wumpus World 中，第 7 章的混合智能体选择了"只走能被证明安全的格子"——fail-safe。这个设计原则应当被写入 AI Agent 的动作授权层。

收束：本章看似是一堆技术算法，但它教给我们的元级教训是——可靠性、完备性、效率、表达力四者不可兼得。任何声称"全都要"的系统，一定在某处偷偷放弃了什么。识别出它放弃了什么，是评估任何 AI 推理系统的第一步。