命题逻辑的自动推理

知识库存放句子，推理算法根据这些句子回答查询。核心问题是：知识库的每个模型是否都满足查询？本篇沿着 FIT3080 的模型检查、Horn 子句、链式推理和归结反驳路线展开，再补上一段 SAT 求解的入门衔接 [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5., [2][2] S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020.。阅读前应先通过形式逻辑与自然演绎分清语义后承与语法推导。

本篇始终假定知识库 $K$ 有限，且属于命题逻辑。$K\land\neg q$ 表示把知识库中所有句子与查询的否定取合取。正是有限命题逻辑这一限制，保证了下文穷尽搜索过程的终止；不能把它直接推广到不受限制的一阶逻辑。

把后承问题变成寻找反例

关键转换是

$$K\models q \quad\Longleftrightarrow\quad K\land\neg q\text{ 不可满足}.$$

右边公式的一组满足赋值，恰好就是让 $K$ 成立、让 $q$ 不成立的反模型。它反驳的是后承关系，不是断言查询在每个模型中都为假。反过来，若证明这个公式不可满足，就排除了所有反模型。

对 $n$ 个命题变量，真值表算法枚举 $2^n$ 组赋值，逐一检查：若所有前提为真，查询是否也真？找到反模型就返回“不后承”及其赋值；穷尽所有赋值仍没有反模型，才返回“后承”。单次求值可以机械完成，但赋值数量随变量数指数增长。

例不后承不等于为假

令 $K=\{A\to B\}$，查询为 $B$。$A$ 假、$B$ 假是反模型，所以 $K$ 不后承 $B$。但 $A$ 真、$B$ 真也满足 $K$，因此 $K$ 同样不后承 $\neg B$。目前的信息不足以决定这一点。

矛盾的知识库在经典逻辑中后承一切。解释一个肯定答案时，应区分“结论来自相容的前提”和“前提根本没有模型”。单独检查 $K$ 的可满足性，可以明确这一区别。

子句、CNF 与变换的目的

文字是原子或原子的否定，子句是文字的析取，合取范式 CNF 则是子句的合取。子句集合代表各子句同时成立。空子句 $\square$ 为假，空子句集却为真：空析取没有一个成立的选项，空合取没有施加任何限制。

得到等价 CNF 的常见步骤是消去蕴涵和双条件、把否定向内推进，再将析取对合取分配。例如，

$$A\to(B\land C) \equiv (\neg A\lor B)\land(\neg A\lor C).$$

CNF 是方便推理的表示，不意味着表达式已经最简。直接分配可能让公式指数膨胀。SAT 编码常引入新变量和定义子句，以较小的表示保持可满足性。这种编码与原公式等可满足，但在扩展后的变量集合上未必与原式逻辑等价。

例新变量需要定义约束

引入 $z$ 表示 $A\land B$。定义 $z\leftrightarrow(A\land B)$ 可以编码为

$$(\neg z\lor A)\land(\neg z\lor B) \land(z\lor\neg A\lor\neg B).$$

若要断言被表示的公式为真，还要加入 $z$。仅有定义子句只是连接 $z$ 与输入，并没有要求该表达式成立。

确定子句与 Horn 子句

Horn 子句最多含一个正文字。确定子句恰好含一个正文字，可以改写成“若若干正原子同时成立，则某个正原子成立”的规则：

$$\neg A\lor\neg B\lor C \equiv (A\land B)\to C.$$

事实 $A$ 是规则体为空的确定子句。没有正文字的 Horn 子句表示约束，例如 $A\land B\to\bot$。下面的简单链式算法先限于有限命题确定子句知识库和正原子查询。处理一般 Horn 可满足性时，还需检查是否有约束的规则体被满足。

我们使用下面这个贯穿例子：

$$K=\{A,B,\ (A\land B)\to C,\ C\to D,\ (D\land A)\to E\}.$$

查询是 $E$。每条规则都是蕴涵，不是双条件；知道 $C$，不能反过来从第一条规则推出 $A$ 或 $B$。

前向链：由事实触发规则

前向链从已知事实出发，把规则体已成立的规则头不断加入知识库。在例子中，$A,B$ 触发 $C$，$C$ 触发 $D$，最后 $D,A$ 触发 $E$。当无法再加入新原子时，就到达不动点。

算法 1 有限确定子句知识库的前向链

1:procedure ForwardChain(Facts, Rules, q)

2:$Known \gets Facts$

3:while true do

4:if $q \in Known$ then

5:return true

6:end if

7:$Added \gets \emptyset$

8:for all $(Body \to Head) \in Rules$ do

9:if $Body \subseteq Known$ then

10:$Added \gets Added \cup \{Head\}$

11:end if

12:end for

13:$Added \gets Added \setminus Known$

14:if $Added = \emptyset$ then

15:return false

16:end if

17:$Known \gets Known \cup Added$

18:end while

19:end procedure

这个易读版本可能反复扫描规则。常用的队列实现会为每条规则记录尚未满足的前提数，并建立“某原子出现在哪些规则体中”的索引。每个新原子只处理一次，传播过程连同初始化就能做到与文字出现总次数线性相关。这个复杂度属于带索引的实现，不是任意照着伪代码写出来的实现都自动具备。

每次新增结论都由肯定前件式保证可靠。终止时得到确定子句理论的最小模型：每个模型都必须包含初始事实及逐步触发的结论，而闭合后的集合本身又满足每条规则。因此，不在其中的正原子不被知识库后承。但没有推出它，仍不意味着推出了它的否定。

后向链：由查询生成子目标

后向链从 $E$ 开始。支持它的规则需要 $D$ 和 $A$；证明 $D$ 需要 $C$；证明 $C$ 需要 $A$ 和 $B$，而二者都是事实。一条规则的规则体是 AND 要求，同一规则头的多条规则则是 OR 备选路径。选中的一条路径必须完成全部前提。

朴素深度优先实现可能陷入循环，例如 $A\to B$ 与 $B\to A$。重复目标需要循环处理，共享子目标可以使用表格化记录。某目标在当前递归栈上被阻塞，不能据此永久缓存为全局失败，因为其他规则或后续事实可能支持它。有限命题情况下，结合不动点传播的表格化方法或适当的完备搜索，可以得到全部确定子句后承；规则系统完备并不意味着任意搜索顺序都完备。

需要许多结论或反复查询时，前向链可能更合适；只关心特定目标时，后向链可以避免推导无关事实。没有哪一个方向总是更快。FIT3080 在进入一般子句推理之前，先介绍这两种方法 [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5.。

归结反驳

归结把含有互补文字的两个子句组合起来：

$$\frac{C\lor L\qquad D\lor\neg L}{C\lor D}.$$

若 $L$ 假，第一个父子句要求 $C$ 成立；若 $L$ 真，第二个父子句要求 $D$ 成立。无论哪种情况，$C\lor D$ 都真，这就是规则的可靠性理由。每次消去选定的一对互补文字，保留其余文字并去重，不能一次删除几组互不相关的互补文字。

证明完整的命题逻辑归结反驳

令 $K=\{A\to B,B\to C,A\}$，查询为 $C$。把前提变成子句，并加入查询的否定。

子句	公式	来源
1	$\neg A\lor B$	第一个前提
2	$\neg B\lor C$	第二个前提
3	$A$	事实
4	$\neg C$	查询的否定
5	$B$	对 1、3 中的 $A$ 归结
6	$C$	对 2、5 中的 $B$ 归结
7	$\square$	对 4、6 中的 $C$ 归结

每一步都注明父子句及选定文字。空子句说明 $K\land\neg C$ 不可满足，因此 $K\models C$。

要把规则变成判定过程，需要不断生成新归结式、保留结果并避免重复。命题变量有限时，不同的非重言子句也只有有限多个。完备的饱和过程要么得到空子句，要么在没有空子句的情况下达到不动点；后一种情况说明子句集可满足。若只是在达到不动点之前超时，两个结论都不能下。

归结具有反驳完备性：不可满足的命题子句集一定存在归结反驳。这并不意味着向前不断归结就会直接列出每一个被后承的任意公式。回答后承查询时，应先否定查询，再寻找反驳。

证明命题归结的反驳完备性

对原子数归纳。没有原子时，子句集不可满足当且仅当含空子句。归纳步选原子 $p$：保留所有不含 $p$ 的子句，并对每一对 $p\lor C$、$\neg p\lor D$ 加入归结式 $C\lor D$，丢弃重言式，得到变量更少的 $S'$。

原子句集的模型由归结可靠性必满足 $S'$。反过来，给定 $S'$ 的模型，只有当 $C$ 为假时，$p\lor C$ 才强迫 $p$ 为真；只有当 $D$ 为假时，$\neg p\lor D$ 才强迫 $p$ 为假。两种要求不可能同时出现，否则对应的归结式也为假，而且不会是重言式。按要求选择 $p$，没有要求时任取，就把模型扩展到原子句集。因此消元保持可满足性。

若原集合不可满足，$S'$ 也不可满足。由归纳假设可反驳 $S'$；它的每个子句要么原本就有，要么由一次归结得到，所以把这些步骤接在前面便得到原集合的反驳。$n$ 个原子至多有 $3^n$ 个非重言子句，因为每个原子只有“不出现、正文字、负文字”三种状态。因此饱和过程有限，且由完备性，无空子句的饱和集合必可满足。

SAT 搜索：用 DPLL 理解一个小型判定过程

SAT 求解器判断命题公式是否存在满足赋值。DPLL 在 CNF 上工作，通过部分赋值化简子句，反复进行单位传播，必要时再分支。单位子句要求其中唯一剩余的文字为真；出现空子句表示冲突，没有剩余子句则说明原先各子句已被部分赋值满足。

算法 2 有限命题子句集上的 DPLL

1:procedure DPLL(S)

2:$S \gets$ UnitPropagate($S$)

3:if $\square \in S$ then

4:return false

5:end if

6:if $S = \emptyset$ then

7:return true

8:end if

9:从 $S$ 中选择尚未赋值的原子 $p$

10:if DPLL($S[p:=true]$) then

11:return true

12:end if

13:return DPLL($S[p:=false]$)

14:end procedure

这里的限制操作删去已满足的子句，并从其余子句中删去已为假的文字。单位传播反复对单位文字执行这个操作，直到没有单位子句或出现冲突。每次分支都会为一个新原子赋值，因此有限搜索一定终止。伪代码只返回布尔值；真正要输出模型，还需保留并返回沿途累计的赋值。

对 $(A\lor B)\land(\neg A\lor C)\land\neg C$，单位传播先要求 $C$ 假，再要求 $A$ 假，最后要求 $B$ 真，各子句于是都被满足。若再加入 $\neg B$，就会产生冲突，说明公式不可满足。现代 SAT 求解器还加入冲突驱动的子句学习等机制；这里的基本过程用于理解逻辑原理，不代表现代求解器的全部性能来源。

证明DPLL 的正确性

每个模型都必须使单位文字为真，所以按它限制公式保持可满足性。对剩余原子 $p$，任何模型都把它取成真或假，因此当前集合可满足，当且仅当两个限制分支中至少一个可满足。空子句没有模型，空子句集则接受当前赋值的任意扩展，这给出递归基例。对未赋值原子数归纳，就证明布尔返回值正确；每次传播或分支都消去未赋值原子，同一个有限度量也证明终止。

一个小型定理证明器应记录什么

最小的命题逻辑后承工具需要输入语言、保持语义或恰当保持可满足性的编码、推理或搜索引擎，以及可以解释的结果。反模型应对照原始前提和查询检查。归结证明证书应记录父子句和消去的文字，并以空子句结束。独立检查器可以逐步验证证书，无需重跑当时的搜索。

这里要区分寻找证明与检查证明。局部规则合法，不代表搜索策略有效；搜索很快，也不能替代结论检查。SAT、UNSAT 和搜索未完成必须是不同结果。对于后承问题，$K\land\neg q$ 的 SAT 结果给出反模型，UNSAT 结果才建立后承关系。

练习

练习识别逻辑片段

把 $A$、$\neg A\lor B$、$\neg A\lor\neg B$、$A\lor B$ 分为确定子句、非确定的 Horn 子句或非 Horn 子句。

查看解析

解

前两个恰好含一个正文字，是确定子句。第三个没有正文字，是非确定的 Horn 子句，可表示约束。第四个有两个正文字，不是 Horn 子句。

练习不要反向使用规则

对 $\{A,A\to B,(B\land C)\to D\}$ 做前向链，查询 $D$。能推出什么？没有推出 $D$ 意味着什么？

查看解析

解

最小模型包含 $A,B$。没有规则提供 $C$，所以推不出 $D$，知识库也不后承 $D$。但它不后承 $\neg D$，因为四个原子全真也满足知识库。不能把结论为 $D$ 的规则倒过来使用，从中擅自推出 $C$。

练习构造归结反驳

由 $P\lor Q$、$P\to R$ 和 $Q\to R$，使用归结反驳证明 $R$。

查看解析

解

子句为 $P\lor Q$、$\neg P\lor R$、$\neg Q\lor R$，再加入查询的否定 $\neg R$。第二、第四个子句归结得到 $\neg P$，第三、第四个得到 $\neg Q$。用 $P\lor Q$ 与 $\neg P$ 得到 $Q$，再与 $\neg Q$ 得到空子句。

练习搜索截断不是反模型

归结搜索执行一百步后停止，没有得到空子句。此时能否报告查询不被后承？

查看解析

解

不能。步数上限不等于达到饱和，后续步骤仍可能找到反驳。此时应报告未完成或未知。找到并验证否定查询问题的满足赋值，才足以报告“不后承”；完整的有限饱和过程也可以作出判定。

下一步：变量、见证与合一

命题逻辑把每个原子视为不可再分的整体。要对对象、关系和量化规则进行推理，就进入一阶逻辑的归结与定理证明。规则与搜索的区别仍然存在，但终止性不再自动成立。

参考文献

1. [1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5. a b
2. [2] S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020. ↩