logic - 分辨率证明 - 人工智能

Question

我正在做一个我需要展示的练习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，但从那里开始，我不知道如何走得更远。将不胜感激任何帮助。谢谢！

Answer 1

一般解析规则是，对于任何两个子句（即文字的析取）

P_1 v ... v P_n

和

Q_1 v ... v Q_m

在您的 CNF 中存在 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),

通过连接两个子句，同时删除对立的Band ¬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是其子句之一，¬D由 CNF 暗示。由于 CNF 等价于原始 KB，因此 KB 意味着¬D.