通過決議證明 - 人工智能

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。