AI筆記34 - Logical representation of Wumpus world

Wumpus world revisited

我們現在可以用proposition來表示目前的wumpus world knowledge:

一開始player在 (1,1)，可以得到以下的true propositions:

R5是後來player 跑到 (2,1)的truth。

Entailment vs Inference

這邊要先釐清的觀念是 entailment和inference的定義。
entailment符號寫成如下:

entailment的語意(semantics)是 某個sentence alpha如果為真，則藉由model checking必須要一 一檢視KB中所有的models / truth tables都為真，但是running time可能是exponential，上面讀法為 alpha models KB或是KB entails alpha。

entailment語法(syntax)上是利用theorem proving，也就是利用某些rules對KB中的knowledge去做inference，看是否能達到alpha為真，而不必一 一檢視所有的models，符號上寫為:

這讀法就是KB implies / infers alpha。

我們要一個inference algorithm可以達到:
1. sound (正確性): 只要infer出truth, 不要false (廢話)，但是infer出來的truth必須要能和KB一致(entailment):

所以如果某個inference演算法能從KB infer出某個sentence alpha (且為true)，則其必須要包含在KB entailed alpha的set中。

2. complete(完整性): 所有的entailed sentence都希望能被infer出來:

所以這兩個set其實是互相包含，也就是相等。
inference就是要找出所有entailed sentences。

所以什麼是Model checking?

假設某一個Knowledge base KB是由五個rules {R1,R2,R3,R4,R5}組成，所以KB要entails某個sentence alpha只有當這個alpha讓所有KB rules為真時。

假設我們的wumpus world有以下7個alpha (propositions)，model checking的方法就是我們用truth table assign各種true false，看什麼時候這7個proposition會讓KB entails:

首先可以看到truth table中，KB (R1 && R2 && ... && R5)為true時只有三個entry，但是只有B2,1是全部assignment為true，也就是不管其他alpha是什麼boolean value，B2,1 永遠都只有true的時候才能讓KB為true。所以我們發現了KB entails B2,1。

另外B1,1 P1,1 P1,2 P2,1 都是在false的時候能讓KB為true，所以我們也可以說KB entails這些alpha的negation。

至於P2,2 P3,1 true or false都有可能讓KB為true，所以不符合entailment的定義。

Theorem Proving

model checking要把所有的KB中的sentences/models都列出來，並且加上alpha的truth assignment形成一個truth table，另一個不這樣做的方法就是利用inference，稱為theorem proving。

首先假設KB是由以下5個rules組成:

如果我們要ASK以下的問題，該怎麼從KB去infer答案出來?\

首先只有R2有跟P1,2和P2,1有關，先從這邊下手(有沒有search意味?)
R2是一個iff proposition，也是biderectional proposition，事實上可以拆成兩個propositions:

ok, 我們可以看到R4有一個 -B1,1，所以我們可以把第一個proposition用demorgan's law來改寫:

注意，這時候我們有一個modus ponens inference 出現:
p: R4
q: -P1,2 && -P2,1
p -> q :就是上面demorgan's law改寫的

這樣因為p為真，且p->q為真，則q為真，所以-P1,2 為真，且 -P2,1為真
答案已經揭曉了，P1,2 為false， P1,2也為false。

我們也可以說KB entails -P1,2, KB entails -P2,1。

以上的過程稱為proof by resolution.

以上的過程其實類似search，一開始initial state就是KB，而goal就是我們要prove的sentence，也就是要找出sentence是否能被KB entail。隨著inference的進行得到更多的sentence，KB被增益了，更多的sentence等待被infer，就像是legal moves變多了。