AI筆記35 - Resolution & CNF

Proof by resolution

再來舉Wumpus world來說明怎麼做Proof by resolution.
首先我們有以下的KB:

player一開始在1,1，後來跑到2,1，再來跑到1,2，觀察到以上的KB中的sentences。
在infer過程中，會出現一個特殊的form:

可以看到 P11 OR P22 OR P31   AND  -P22

這是一個conjunction (AND) 連結兩個 OR形成的clause （右邊-P22 也可以看成 -P22 OR True)
但是-P22和　P22互斥，由於-P22為True，則P22只能為False。

這邊　-P22 和 P22 這兩個element "resolved" ，做了一個resolution，形成了一個新的true的sentence: P11 OR P31，稱為一個"resolvent"。

當然最後可以得出KB entails P31，因為player在1,1出發，而那邊沒有pit：

以上resolution過程稱為 "unit resolution"，general form如下：

Conjunctive Normal Form (CNF)

unit resolution可以延伸到更general的兩個clause:

以上兩個clauses都同時為真，這種由兩個disunction clauses組成的AND 關係，稱為CNF，例如：

如果對這種CNF apply resolution rule，一定會找出sound and complete inference results。

IFF Implication proposition轉換成CNF

假設有一個iff proposition:

iff proposition可以先拆成兩個方向的implication：

然後implication 和 -a OR b是logically equivalent:

不過右邊還不是完全的disjunction，採用demorgan's law把negation符號展開：

並且用分配律把所有Disjunction clause用conjunction 連接:

這樣就完成了我們的CNF。

Resolution algorithm (proof by contradiction)

以下是一個利用CNF form來做resolution的演算法：

為了要檢視是否KB entails alpha，演算法假設KB  entails -alpha 成立，如果發現矛盾代表KB entails alpha，為什麼要採用反證法？

因為這樣才有辦法用之前提到的unit resolution，才能做resolution。
所以如果沒有任何resolvents出現，代表KB && -alpha所形成的CNF中任意兩個 clause無法resolve出任何東西，亦即KB　&& -alpha沒有產出新的sentence，當然就證明 KB 不entail -alpha，意即反證KB entails alpha。


舉例來說，我們想知道某個KB是否entails alpha:

要用此演算法，我們得假設KB entails -alpha，意即 KB &&-alpha成立：

先把KB && -alpha寫成 CNF:

光是第一個和第二個clause就能產出兩個resolvents，就按照演算法iteratively試著做resolution。
最後發現 -alpha這個clause無法和已經resolve出來的所有新的sentences找出resolvent，代表 KB &&-alpha not satisfying，意即 KB entails alpha。