我正在做一个练习，我需要显示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，但从那里，我不知道如何走得更远。非常感谢任何帮助。谢谢!
一般的解析规则是，对于任意两个子句(即字面的析取)
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),
将两个子句连接起来，去掉相反的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 v ¬D解析这个新子句¬B，得到¬D。
因为CNF是一个连接词，它成立的事实意味着它中的每个子句都成立。也就是说，CNF包含了它的所有条款。因为¬D是它的子句之一，所以¬D是由CNF隐含的。由于CNF等价于原始KB，因此KB暗示¬D。