一阶逻辑的合取范式

9.5.1 一阶逻辑的合取范式

如同在命题逻辑中，一阶逻辑的归结也要求语句必须是合取范式（CNF）——即子句的合取式，其中每个子句是文字[33]的析取式。文字可以包含变量，假设这些变量是全称量化的。例如，语句

以CNF表示，变成

¬American(x)∨¬Weapon(y)∨¬Sells(x,y,z)∨¬Hostile(z)∨Criminal(x)

一阶逻辑的每个语句都可以转换成一个推理等价的CNF语句。特别是，CNF 语句只有当原始语句不可满足时才不可满足，因此我们证明的基础是CNF语句上的反证法。

转换到CNF的过程和命题逻辑的情况非常类似，我们可以参考第7.5.2节。主要的不同来自消除存在量词的要求。我们将通过转换语句“Everyone who loves all animals is loved by someone（爱所有动物的每个人会被某人爱）”来说明这个过程，或者写为

步骤如下所示：

消除蕴含：

∀ x [¬∀ y ¬Animal(y)∨Loves(x, y)] ∨ [∃y Loves(y, x)]

将¬内移：除了用于否定连接符的通用规则之外，我们还需要否定量词的规则。因此，我们有

¬∀ x　p　　　 变成　　∃x　¬p

¬∃x　p　　　 变成　　∀ x　¬p

我们的语句经过以下变形：

∀ x [∃y ¬ (¬Animal(y)∨Loves(x, y))] ∨ [∃y Loves(y, x)]

∀ x [∃y ¬¬Animal(y)∧¬Loves(x,y)] ∨ [∃y Loves(y,x)]

∀ x [∃y Animal(y)∧¬Loves(x, y)] ∨ [∃y Loves(y, x)]

注意蕴涵前提中的全称量词（∀ y）是怎样转变成存在量词的。现在，语句被解读为“或者存在x不喜爱的某种动物，（如果这不是事实）或者某人喜爱x（Either there is some animal that x doesn’t love, or (if this is not the case)someone loves x.）。”很清楚，原始语句的意思保留了下来。

变量标准化：对于那些使用相同变量名两次的语句诸如(∀ x P(x))∨(∃x Q(x))，改变其中一个变量名。这可以避免后续步骤在去除量词之后的混淆。这样，我们得到

∀ x [∃y Animal(y)∧¬Loves(x, y)] ∨ [∃z Loves(z, x)]

Skolem化：Skolem化是通过消元法消除存在量词的过程。在简单情况下，它就类似于第9.1节中的存在实例化规则：将∃x P(x)转换成P(A)，其中A是一个新的常量。不过如果我们将这条规则应用于我们的简单例句，则可以得到

∀ x [Animal(A)∧¬Loves(x, A)] ∨ Loves(B, x)

它的意思是完全错误的：它表明每个人或者不爱某种特定的动物 A，或者被某个特定的实体B 爱上。事实上，初始的语句允许每个人可以不喜爱某种不同的动物，或者被不同的某人爱上。因此，我们希望Skolem实体依赖于x：

∀ x [Animal(F(x))∧¬Loves(x, F(x))] ∨ Loves(G(x), x)

其中，F和G为Skolem函数。通用规则是Skolem函数的参数都是全称量化变量，要消去的存在量词出现在这些变量的作用域中。和存在实例化一样，当原始语句可满足时，Skolem化语句也恰好可满足。

去除全称量词：在这一点上，所有保留下来的变量必须都是全称量化的。而且，语句等价于所有全称量词都已经移到左侧的语句。因此，我们可以去除全称量词：

[Animal(F(x))∧¬Loves(x, F(x))] ∨ Loves(G(x), x)

将∧分配到∨中：

[Animal(F(x))∨Loves(G(x), x)] ∧ [¬Loves(x, F(x))∨Loves(G(x), x)]

这一步也可能需要展开嵌套的合取式和析取式。

现在，语句是包括两个子句的CNF了。它可读性很差。（这样表述可能有助于解释：Skolem函数F(x)指x可能不喜欢的动物，而G(x)指那些可能爱上x的人。）幸运的是，人类很少需要查看CNF语句——翻译过程很容易自动进行。