我正在做一个练习，需要证明 KB |= ~D。

我知道知识库是这样的：

 - (B v ¬C) => ¬A - (¬A v D) => B - A ∧ C

转换为CNF之后：

A ∧ C ∧ (¬A v ¬B) ∧ (¬A v C) ∧ (A v B) ∧ (B v ¬D)

现在我已经转换成了CNF，但接下来不知道该怎么做。希望能得到一些帮助。谢谢！

回答：

一般归结规则是，对于你的CNF中的任意两个子句（即文字的析取）

P_1 v ... v P_n

和

Q_1 v ... v Q_m

如果存在i和j使得P_i和Q_j互为否定，你可以添加一个新的子句

P_1 v ... v P_{i-1} v P_{i+1} ... v P_n v Q_1 v ... v Q_{j-1} v Q_{j+1} ... v Q_m

这只是一个严格的方式来说明你可以通过连接两个子句，减去一个在每个子句中具有相反“符号”的文字来形成一个新的子句。

例如

(A v ¬B)∧(B v ¬C)

等价于

(A v ¬B)∧(B v ¬C)∧(A v ¬C),

通过连接这两个子句并移除相反的B和¬B，得到A v ¬C。

另一个例子是

A∧(¬A v ¬C)

这等价于

A∧(¬A v ¬C) ∧ ¬C.

因为A算作一个只有一个文字的子句（即A本身）。所以这两个子句被连接，而A和¬A被移除，产生一个新的子句¬C。

将此应用到你的问题中，我们可以归结A和¬A v ¬B，得到¬B。然后我们用这个新的子句¬B和B v ¬D进行归结，得到¬D。

因为CNF是一个合取，它成立的事实意味着其中的每一个子句都成立。也就是说，CNF暗示了它的所有子句。由于¬D是它的子句之一，CNF暗示了¬D。由于CNF等价于原始的KB，所以KB暗示了¬D。