人工智能第四章.ppt

1、Chapter 4. Resolution,4.1 Clausal Form 4.2 Unification 4.3 Resolution Principle 4.4 Resolution Procedure 4.5 Unsatisfactory,Chapter 4. Resolution (continued),4.6 True-or-False Questions 4.7 Fill-in-the-Blank Questions 4.8 Circuit Example 4.9 Mathematics Example 4.10 Soundness and Completeness 4.11 R

2、esolution and Equality,歸結(jié),對于定理證明問題，可以用一階謂詞邏輯表示，即給定前提P和結(jié)論Q，證明PQ。 需要對每一個解釋進行驗證。 可以使用上一章的推理過程進行推理。 但是中間結(jié)果數(shù)量龐大，而且可能無法推理出。 采用反證法。 PQ。,4.1 Clausal Form,子句型是一種簡化了的謂詞演算，除了普通謂詞演算符號外，還包括文字和子句。 文字：原子謂詞公式及其否定統(tǒng)稱為文字 子句：任何文字的析取式稱為子句 空子句：不包含任何文字的子句稱為空子句記為：或NIL Horn子句：至多包含一個正文字的子句。 子句集：由子句和空子句所構(gòu)成的集合稱為子句集,子句型的生成過程,（1

3、）刪除蘊涵符 （2）否定內(nèi)移 （3）變量標準化 （4）刪除存在量詞 （5）刪除全稱量詞 （6）析取內(nèi)移 （7）刪除合取運算符 （8）變量更名,演示示例,演示示例（續(xù)）,同一變量只受 一個量詞約束,演示示例（續(xù)）,（4）刪除存在量詞,skolem函數(shù)：該函數(shù)的變元就是由那些全稱量詞所約束的全稱量詞量化的變量.Skolem函數(shù)所使用的函數(shù)符號必須是新的.,演示示例（續(xù)）,（5）析取內(nèi)移（化為合取范式） （6）刪除全稱量詞,演示示例（續(xù)）,（7）刪除合取運算符 （8）變量更名,4.2 Unification,合一：判定兩個表達式通過適當?shù)闹脫Q是否可以變成同一表達式的過程。 置換： 形如 建立了一個變

4、量與表達式之間的關(guān)聯(lián) 每一個變量至多與一個表達式相關(guān)聯(lián) 被關(guān)聯(lián)的變量不出現(xiàn)在任何關(guān)聯(lián)的表達式中 如：A/x, F(B)/y, w/z 是置換；G(y)/x, F(x)/y不是置換。,Term,項是論域中的對象名，定義如下： 單獨一個個體（常量或變量）是項； 若t1, t2, , tn是項，f 是n 元函數(shù)，則f (t1, t2, , tn )是項； 由1,生成的表達式是項。 因此，項有三種類型：變量、常量或者函數(shù)表達式。,置換實例（例示）,置換的合成,設(shè),合成運算舉例,合一,合一,合一不一定唯一 E=P(a,y), P(x, f(b) 1=a/x, f(b)/y (唯一) E=P(x,y),

5、P(x,f(b) 1=a/x, f(b)/y (不唯一) 2=b/x, f(b)/y,合一運算舉例,差異集合,設(shè)W是非空表達式集合，W的差異集合D定義如下：首先找出W的所有表達式中不是都相同的第一個符號，然后從W的每個表達式中抽出占有這個符號位置的子表達式，所有這些子表達式組成的集合就是W的差異集合D。 例子: W=P(x,f(y,z),z，w), P(x,a), P(x, g(z),z,b) D=f(y,z), a, g(z),合一算法（1）,(1)令k=0, W0=W(W=E1, E2), 0= (2)如果Wk已經(jīng)合一,則算法停止, k=mgu 否則，求出Wk的差異集Dk (3)如果Dk中

6、存在元素xk , tk,xk是變元,tk是項,且xk不在tk中出現(xiàn),則轉(zhuǎn)(4)；否則不可合一，停止 (4)令 k+1= k tk /xk W k+1= W ktk /xk=W k+1 k=k+1 然后轉(zhuǎn)(2) (5)算法終止，mgu不存在。,合一算法（2）,換名: P(f(x), x), P(x, a); 如果不換名：D=f(x), x. 換名: P(f(y), y), P(x, a); mgu: f(a)/x, a/y,合一算法（3）,求W=P(a,x,f(g(y), P(z,f(z),f(u)的mgu. D0=a,z， 1= a/z= a/z. W1= W0 1 =P(a,x,f(g(y)

7、, P(a,f(a),f(u) D1=x,f(a)， 2= 1 f(a)/x= a/z, f(a)/x. W2= W1 2 =P(a,f(a),f(g(y), P(a,f(a),f(u) D2=g(y),u， 3= 2 g(y)/u=a/z,f(a)/x, g(y)/u W3= W2 3 =P(a,f(a),f(g(y) 3是mgu.,合一算法（4）,求W=Q(f(a), g(x), Q(y, y)的mgu. D0=f(a),y， 1= f(a)/y= f(a)/y. W1= W0 1 =Q(f(a), g(x), Q(f(a), f(a) D1=g(x), f(a). 不可合一, 沒有mgu

8、.,合一算法（5）,求W=P(f(y), y), P(x, a)的mgu. D0=f(y),x. 1= f(y)/x= f(y)/x. W1= W0 1 =P(f(y), y), P(f(y), a) D1=y, a. 2= 1 a/y= f(y)/x a/y = f(a)/x, a/y. W2= W1 2 =P(f(a),a) 2是mgu.,4.3 Resolution Principle,（1）不含變量的歸結(jié),（2）帶合一操作的歸結(jié),歸結(jié)式可能不唯一,子句的因子,問題： 應(yīng)該能歸結(jié)出 ，但利用前面的過程不能實現(xiàn)。 利用子句因子的歸結(jié)來解決。 如果子句中的文字的一個子集有mgu , 則將應(yīng)用

9、于所得的結(jié)果=稱為的一個因子。 舉例： = 其中， 有mgu = 是的一個因子。,歸結(jié)原理的定義,如果兩個子句和的兩個因子和可以歸結(jié)，則可將其歸結(jié)式作為和的歸結(jié)式。,利用子句因子的歸結(jié)解決上頁中的問題：,4.4 Resolution Procedure,Definition Example:,Resolution procedure,Breadth first,Resolution graph,附加過程,可以用來擴展歸結(jié)推理過程。 可以用來化簡子句，P, Q, R，若已知R為真。則確定這個子句永真。 永真子句可以從子句集中刪掉。 永假文字可以從子句中刪掉。,4.5 Unsatisfactory

10、,歸結(jié)推理最簡單的應(yīng)用就是驗證不可滿足性。如果一個子句集是不可滿足的，則總可以通過歸結(jié)從該子句集推導出矛盾，即空子句。 利用歸結(jié)推理也可以驗證邏輯蘊涵。 |= ，根據(jù)反演定理，只需證明不一致，即不可滿足。 步驟：（1） 將 加入到中，得到；（2）將轉(zhuǎn)換成子句型；（3）對子句型進行歸結(jié)，若得到空子句，則不可滿足，即 |= 。該過程稱為歸結(jié)反演推理。,模型的視角,如果 |= ，則的所有模型都是的模型。因此，這些模型里沒有的模型。因此 不可滿足。 反之，假設(shè) 不可滿足，而可滿足。令I(lǐng)是滿足的一個解釋，I不可滿足。因此， I滿足。因為I是任意的，所以所有滿足的解釋都可滿足I，因此的模型都是的模型，即

11、|= 。,4.6 True-of-False Questions,1.F(Art, Jon) 2.F(Bob, Kim) 3F(x, y), P(x, y) 4.P(Art, Jon) 5.P(Art, Jon)1,3 6.P(Bob, Kim)2,3 7.F(Art, Jon)3,4 8.4,5 9.1,7,重言式的證明,F(Art, Jon) F(Art, Jon),4.7 Fill-in-the Blank Questions,要回答誰是Jon的父母 引入自由變量x P(x, Jon) 目標是推出x是什么 為要回答的引入answer文字 Ans(1, ., n)，1, ., n是中的自由

12、變量 x P(x, Jon) Ans(x) 化為子句型，加入前提進行歸結(jié),4.7 Fill-in-the Blank Questions,1.F(Art, Jon) 2.F(Bob, Kim) 3F(x, y), P(x, y) 4.P(z, Jon), Ans(z) 5.P(Art, Jon)1,3 6.P(Bob, Kim)2,3 7.F(w, Jon), Ans(w)3,4 8.Ans(Art)4,5 9.Ans(Art) 1,7,4.7 Fill-in-the Blank Questions,1.F(Art, Jon) 2.M(Ann, Jon) 3.F(x, y), P(x, y)

13、4.M(u, v), P(u, v) 5.P(z, Jon), Ans(z) 6.P(Art, Jon)1,3 7.P(Ann, Jon)2,4 8.F(s, Jon), Ans(s)3,5 9.M(t, Jon), Ans(t)4,5 10.Ans(Art)5,6 11.Ans(Ann)5,7 12.Ans(Art) 1,8 13.Ans(Ann)2,9,The disadvantage of Resolution,Dont know when will the resolution stop. Due to the undecidatilty of logical implication, we can never know whether we have found all the possible answers. In some ca