通过决议证明 - 人工智能

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 

在CNF这样

和

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) 

是通过连接两个子句，同时除去对立B和¬B，获得A v ¬C相当于

(A v ¬B)∧(B v ¬C)∧(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。