第 11 讲 · 谓词归结、统一与 Herbrand 方法

谓词归结的目标仍是推出空子句，但 $P(x)$ 与 $\neg P(a)$ 不是字面相同的互补文字。必须先找到代换使它们统一。

从公式到谓词子句集

证明 $\Gamma\models R$ 的完整预处理是：

1. 加入 $\neg R$；
2. 消去 $\to,\leftrightarrow$；
3. 把否定推进原子公式；
4. 标准化变量名；
5. 化为前束范式；
6. Skolem 化消去存在量词；
7. 省略最前面的全称量词；
8. 把母式化为 CNF；
9. 拆成子句集。

Skolem 化只保持可满足性，恰好足够用于反驳：原集合不可满足，当且仅当正确 Skolem 化后的集合不可满足。

代换与统一

代换写成

$$\theta=\{x/t,\ y/s,\ldots\}.$$

将它同时作用于公式或子句中的自由变量。

例如

$$P(f(x),x)$$

与

$$P(f(a),a)$$

可由

$$\theta=\{x/a\}$$

统一。

但

$$P(x)$$

与

$$P(f(x))$$

不能用有限项代换统一，因为要求 $x=f(x)$ 会让 $x$ 包含自身。这就是 occurs check。

最一般统一子 MGU 保留最多自由度。若 $\{x/y\}$ 已能统一，就不应一开始把 $x,y$ 都代成某个常元，虽然那也可能统一，但失去了通用性。

谓词归结规则

若子句 $C_1,C_2$ 中分别有文字 $L_1,\neg L_2$，且代换 $\theta$ 使

$$L_1\theta=L_2\theta,$$

则可先删去这对文字，再对剩余部分应用 $\theta$：

$$\frac{L_1\lor C_1,\quad\neg L_2\lor C_2} {(C_1\lor C_2)\theta}.$$

每次要写清：

• 两个父子句；
• 选中的互补文字；
• 统一代换 $\theta$；
• 归结子句。

完整例子

证明：

每个学生都喜欢某门课程；没有学生喜欢文学。因此，不是每个学生都喜欢文学。

设 $S(x)$ 表示学生，$L(x,y)$ 表示 $x$ 喜欢 $y$，常元 $lit$ 表示文学。

前提可写为

$$\forall x\bigl(S(x)\to\exists yL(x,y)\bigr),$$ $$\forall x\bigl(S(x)\to\neg L(x,lit)\bigr).$$

若还给出存在学生

$$\exists xS(x),$$

要证明

$$\neg\forall x\bigl(S(x)\to L(x,lit)\bigr).$$

Skolem 化前提并否定结论后可得到一组代表性子句：

$$\neg S(x)\lor L(x,f(x)),$$ $$\neg S(x)\lor\neg L(x,lit),$$ $$S(a),$$

以及否定结论产生的相应约束。由 $S(a)$ 与第二个子句得到

$$\neg L(a,lit).$$

而若否定结论要求所有学生都喜欢文学，则又可得到

$$L(a,lit),$$

最后归结出 $\square$。

这个例子也说明：若没有“至少存在一个学生”，全称陈述可能因学生集合为空而真，结论未必成立。论域非空不代表 $S$ 关系非空。

Herbrand 域

Herbrand 方法把谓词逻辑的对象先限制为语言中能写出的基项。

若语言有常元 $a$ 和一元函数 $f$，Herbrand 域为

$$H=\{a,f(a),f(f(a)),\ldots\}.$$

若语言没有常元，通常补一个新常元以保证域非空。

子句的基实例是用 Herbrand 域中的基项替换全部变量得到的。例如

$$P(x)\lor R(f(x))$$

有基实例

$$P(a)\lor R(f(a)),$$ $$P(f(a))\lor R(f(f(a))),$$

等等。

为什么 Herbrand 方法能说明完备性

Herbrand 定理把一阶子句集的不可满足性连接到它的基实例：

• 若一阶子句集不可满足；
• 则能在其基实例中找到有限的不可满足部分；
• 把每个基原子暂时视为命题变元；
• 命题归结完备性保证这个有限部分存在反驳；
• 再把该反驳提升回谓词归结。

这不是实际做题时要完整重证的算法，但解释了为什么统一加归结不会漏掉所有可能证明。

可靠、完备与终止

谓词归结是可靠的：推出的每个子句都是父子句的逻辑推论。

它对不可满足性是完备的：不可满足子句集一定存在归结反驳。

但它不是总能快速结束的判定程序。若子句集可满足，盲目枚举归结可能无限进行。这与一阶逻辑“有效性半可判定、总体不可判定”的结论一致。