AI筆記36 - Forward/Backward Chaining , First Order Logic

另一個inference 達到completeness的方法

resolution演算法雖然證明sound and complete，但是其實是exponential running time，跟model checking也是一樣的，因為這涉及了所有KB senetences的pairwaise resolution。

另一個較為簡單的linear time方法稱為forward chaining 以及 backward chaining，這是利用modus ponens運作在horn clauses的方法。記得horn clause是以下形式：

如果線上面的clause都為真，則q可以被implied為真：

Forward Chaining

假設KB中都是literal和horn clauses，例如以下：

想要證明KB entails Q?
我們可以把KB用以下的圖表示：

每個節點代表一個implication，這邊都是兩個facts conjunction implies another fact。所以節點可以標上是有幾個facts在premise中　（implication的箭號左邊部分）:

forward chaining就是從任何一個非目標節點，開始刪除節點上的數字，例如A && B implies L，但是KB中有fact A，所以實際上A &&B節點數字2 可以刪減成1，意即B 單獨就可以implies L：

同時跟A有關的節點也都可以減1。

接下來跟B有關的節點也可以減1，因為KB中有B :

Ｌ現在不需要A &&B去imply也成立了，所以跟L有關的節點也可以繼續減去 1 propagate下去：

最終P也變成fact，所以Q當然也是fact，這整個過程就是horn clause implication的拆除：

Backward Chaining

這是先從Q出發，檢視imply Q的horn clause，然後再一一推回去相關的clause，直到抵達facts A和B (也就是沒有horn clause anymore)，這時再forward check是否能真的推回到Q。

等於graph先從Q往下找factds，找到後再往上檢查到Q。

由於課堂中只是簡單帶過，就不多說了。

backward chaining比forward chaining花費的時間可能比forward chaining來的少，因為他是goal-driven，不是像forward chaining一樣亂槍打鳥。

First-order Logic (first-order意指relation是指object之間，而不是更高層次的relation之間）

比較接近真實語言，多了壹些propositional logic沒有的元素：
1. constants: 用來比對的atoms或是symbols
2. variables: 可以bind meaning的entity
3. functions： 用來描述幾個entity之間的關係
4. 一些符號：數學上都常見，例如所有的 存在一個 之類的

舉例來說：
如果Fly(x) 的意思是 x會飛
bird(x)的意思是 x是鳥
則以下句子代表：所有鳥都會飛

還有幾個例子，都很好理解：