我正在做一个练习，我需要证明 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，但从那里开始，我不知道如何进一步发展。将不胜感激任何帮助。谢谢！
【问题讨论】：
标签： logic artificial-intelligence resolution conjunctive-normal-form
一般的解析规则是，对于任何两个子句 （即文字的析取）
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 是其子句之一，因此 CNF 隐含了¬D。由于 CNF 等价于原始 KB，因此 KB 隐含¬D。
【讨论】：