第三講 經(jīng)典邏輯推理

1、第四章 經(jīng)典邏輯推理4.1 基本概念4.2 自然演繹推理4.3 歸結(jié)演繹推理4.4 與或形演繹推理如何實現(xiàn)推理？邏輯方法是自動證明中常用的方法如何進行邏輯推理？推理的過程怎樣？怎么實現(xiàn)推理？柯南的推理過程觀察結(jié)果n時鐘與分鐘重疊在一起n時間是六點半推理依據(jù)n正常的時鐘如果是六點半，那么時鐘與分鐘應(yīng)該是分開的推理結(jié)果n有人故意移動過時鐘人類的推理可以理解語義人類的推理可以理解語義機器如何進行這樣類似的推理？機器如何進行這樣類似的推理？需要將推理的過程和理解分開，使其形式化需要將推理的過程和理解分開，使其形式化w事實事實w規(guī)則規(guī)則w結(jié)論結(jié)論推理的一般形式已知事實：事實1，事實2，. 規(guī)則：如果 事

2、實1 那么 結(jié)論1 如果 事實2 那么 結(jié)論2 .得到：結(jié)論1，結(jié)論2 將事實與規(guī)則借助一些符號符號來表示，推理過程就可以被形式化 P: 某已知事實 P Q : 如果P，那么Q 結(jié)論：Q符號與形式語言自然語言不適合計算機處理n她用紅紅色水彩筆寫了個藍(lán)藍(lán)字。n小王不方便接電話，他方便去了。需要一種無歧義，方便存儲和表達(dá)的形式化符號表征體系n數(shù)理邏輯符號與形式語言自然語言不適合計算機處理n她用紅紅色水彩筆寫了個藍(lán)藍(lán)字。n小王不方便接電話，他方便去了。需要一種無歧義，方便存儲和表達(dá)的形式化符號表征體系n數(shù)理邏輯w命題邏輯w謂詞邏輯符號與形式語言自然語言不適合計算機處理n她用紅紅色水彩筆寫了個藍(lán)藍(lán)字。

3、n小王不方便接電話，他方便去了。需要一種無歧義，方便存儲和表達(dá)的形式化符號表征體系n數(shù)理邏輯w命題邏輯w謂詞邏輯 w如果不下雨，我就去你家玩P Q w今天沒有下雨 P w我去了你家 Qw凡人都會死 x(Man(x)Mortal(x)w 蘇格拉底是人 Man(Socrates)w 蘇格拉底會死 Mortal(Socrates)4.1 基本概念4.1.1 什么是推理什么是推理所謂推理就是按某種策略由已知判斷推所謂推理就是按某種策略由已知判斷推出另一個判斷的思維過程。出另一個判斷的思維過程。在人工智能中，推理是由程序?qū)崿F(xiàn)的，在人工智能中，推理是由程序?qū)崿F(xiàn)的，稱為推理機。稱為推理機。4.1.2 推理方

4、式及其分類1. 演繹推理、歸納推理、默認(rèn)推理演繹推理、歸納推理、默認(rèn)推理演繹推理：從一般到特殊。例如三段論。演繹推理：從一般到特殊。例如三段論。歸納推理：從個體到一般。歸納推理：從個體到一般。默認(rèn)推理：缺省推理，在知識不完全的情況下假設(shè)某默認(rèn)推理：缺省推理，在知識不完全的情況下假設(shè)某些條件已經(jīng)具備所進行的推理。些條件已經(jīng)具備所進行的推理。2. 確定性、不確定性推理確定性、不確定性推理3. 單調(diào)推理、非單調(diào)推理單調(diào)推理、非單調(diào)推理推出的結(jié)論是否單調(diào)增加推出的結(jié)論是否單調(diào)增加4. 啟發(fā)式、非啟發(fā)式推理啟發(fā)式、非啟發(fā)式推理所謂啟發(fā)性知識是指與問題有關(guān)且能加快推理進程、所謂啟發(fā)性知識是指與問題有關(guān)且能

5、加快推理進程、求得問題最優(yōu)解的知識。求得問題最優(yōu)解的知識。5. 基于知識的推理（專家系統(tǒng)）基于知識的推理（專家系統(tǒng)） 、統(tǒng)計推理、直覺推理、統(tǒng)計推理、直覺推理（常識性推理）（常識性推理）4.1.3 推理的控制策略推理的控制策略主要包括：推理方向、搜索策略、沖推理的控制策略主要包括：推理方向、搜索策略、沖突消解策略、求解策略及限制策略。突消解策略、求解策略及限制策略。1. 正向推理（數(shù)據(jù)驅(qū)動推理）正向推理（數(shù)據(jù)驅(qū)動推理）正向推理的基本思想是：從用戶提供的初始已知事實正向推理的基本思想是：從用戶提供的初始已知事實出發(fā)，在知識庫出發(fā)，在知識庫KB中找出當(dāng)前可適用的知識，構(gòu)成可中找出當(dāng)前可適用的知識，

6、構(gòu)成可適用的知識集適用的知識集KS，然后按某種沖突消解策略從，然后按某種沖突消解策略從KS中選中選出一條知識進行推理，并將推出的新事實加入到數(shù)據(jù)出一條知識進行推理，并將推出的新事實加入到數(shù)據(jù)庫庫DB中，作為下一步推理的已知事實。在此之后，再中，作為下一步推理的已知事實。在此之后，再在知識庫中選取可適用的知識進行推理。如此重復(fù)進在知識庫中選取可適用的知識進行推理。如此重復(fù)進行這一過程，直到求得所要求的解。行這一過程，直到求得所要求的解。正向推理示意圖開始退出把初始已知事實送入DBDB中包含問題的解？KB中有可適用的知識？把KB中所有使用知識都選出來送入KSKS為空？按沖突消解策略從KS中選出一條

7、知識進行推理推出的是新事實？將該新事實加入DB中用戶可補充新事實？把用戶提供的新事實加入DB中YNNYNYNYNY成功失敗 動物識別的例子w已知事實：一動物已知事實：一動物有毛，吃草，黑條紋有毛，吃草，黑條紋nR1：動物有毛：動物有毛 哺乳類哺乳類 nR2：動物產(chǎn)奶：動物產(chǎn)奶 哺乳類哺乳類 nR3：哺乳類：哺乳類 吃肉吃肉 食肉類食肉類 nR4：哺乳類：哺乳類 吃草吃草 有蹄類有蹄類 nR5：食肉類：食肉類 黃褐色黃褐色 有斑點有斑點 獵狗獵狗 nR6：食肉類：食肉類 黃褐色黃褐色 黑條紋黑條紋 虎虎 nR7：有蹄類：有蹄類 長脖長脖 長頸鹿長頸鹿 nR8：有蹄類：有蹄類 黑條紋黑條紋 斑馬斑

8、馬2 逆向推理逆向推理的基本思想是：首先選定一個逆向推理的基本思想是：首先選定一個假設(shè)目標(biāo)，然后尋找支持該假設(shè)的證據(jù)，假設(shè)目標(biāo)，然后尋找支持該假設(shè)的證據(jù)，若所需的證據(jù)都能找到，則說明原假設(shè)若所需的證據(jù)都能找到，則說明原假設(shè)是成立的；若找不到所需要的證據(jù)，則是成立的；若找不到所需要的證據(jù)，則說明原假設(shè)不成立，此時需要另作新的說明原假設(shè)不成立，此時需要另作新的假設(shè)。假設(shè)。逆向推理示意圖開始退出提出假設(shè)該假設(shè)在DB中？該假設(shè)是證據(jù)？在KB中找出所有能導(dǎo)出該假設(shè)的知識送入KS有此事實？該假設(shè)成立該假設(shè)成立，并將此事實存入數(shù)據(jù)庫YNYNNNY從KS中選出一條知識，并將該知識的一個運用條件作為新的假設(shè)目標(biāo)

9、還有假設(shè)？詢問用戶Y動物識別系統(tǒng) r1： if 該動物有毛發(fā)該動物有毛發(fā) then 該動物是哺乳動物該動物是哺乳動物 r2： if 該動物有奶該動物有奶 then 該動物是哺乳動物該動物是哺乳動物 r3： if 該動物有羽毛該動物有羽毛 then 該動物是鳥該動物是鳥 r4： if 該該動物會飛動物會飛 and 會下蛋會下蛋 then 該動物是鳥該動物是鳥 r5： if 該動物吃肉該動物吃肉 then 該動物是食肉動物該動物是食肉動物 r6： if 該動物有犬齒該動物有犬齒 and 有爪有爪 and 眼盯前方眼盯前方 then 該動物是食肉動物該動物是食肉動物 r7： if 該動物是哺乳動物該

10、動物是哺乳動物 and 有蹄有蹄 then 該動物是有蹄類動物該動物是有蹄類動物 r8： if 該動物是哺乳動物該動物是哺乳動物 and 是嚼反芻類動物是嚼反芻類動物 then 該動物是有蹄類動物該動物是有蹄類動物 r9： if 該動物是哺乳動物該動物是哺乳動物 and 是食肉類動物是食肉類動物 and 是黃褐色是黃褐色 and 身上有暗斑點身上有暗斑點 then 該動物是金錢豹該動物是金錢豹 r10： if 該動物是哺乳動物該動物是哺乳動物 and 是食肉類動物是食肉類動物 and 是黃褐色是黃褐色 and 身上有黑色條紋身上有黑色條紋 then 該動物是虎該動物是虎 r11： if 該動物

11、是有蹄類動物該動物是有蹄類動物 and 有長脖子有長脖子 and 有長腿有長腿 and 身上有暗斑點身上有暗斑點 then 該動物是長頸鹿該動物是長頸鹿 r12： if 該動物是有蹄類動物該動物是有蹄類動物 and 身上有黑色條紋身上有黑色條紋 then 該動物是斑馬該動物是斑馬 r13： if 該動物是鳥該動物是鳥 and 有長脖子有長脖子 and 有長腿有長腿 and 不會飛不會飛 then 該動物是鴕鳥該動物是鴕鳥 r14： if 該動物是鳥該動物是鳥 and 會游泳會游泳 and 不會飛不會飛 and 有黑白兩色有黑白兩色 then 該動物是企鵝該動物是企鵝 r15： if 該動物是鳥

12、該動物是鳥 and 善飛善飛 then 該動物是信天翁該動物是信天翁3. 混合推理混合推理先正向推理后逆向推理先正向推理后逆向推理先逆向推理后正向推理先逆向推理后正向推理4. 雙向推理雙向推理正向推理與逆向推理同時進行，且在推理過程正向推理與逆向推理同時進行，且在推理過程中的某一步上中的某一步上“碰頭碰頭”。5. 求解策略求解策略只求一個解，還是求所有解以及最優(yōu)解。只求一個解，還是求所有解以及最優(yōu)解。6. 限制策略限制策略限制搜索的深度、寬度、時間、空間等等。限制搜索的深度、寬度、時間、空間等等。所謂模式匹配是指對兩個知識模式所謂模式匹配是指對兩個知識模式(例如兩個謂詞公例如兩個謂詞公式、框架

13、片斷、語義網(wǎng)絡(luò)片斷式、框架片斷、語義網(wǎng)絡(luò)片斷)進行比較，檢查這兩進行比較，檢查這兩個知識模式是否完全一致或者近似一致。個知識模式是否完全一致或者近似一致。模式匹配可分為確定性匹配與不確定性匹配。模式匹配可分為確定性匹配與不確定性匹配。確定性匹配是指兩個知識模式完全一致，或者經(jīng)過確定性匹配是指兩個知識模式完全一致，或者經(jīng)過變量代換后變得完全一致。變量代換后變得完全一致。 知識：知識：IF father(x,y) and man(y) THEN son(y,x) 事實：事實：father(李四，李小四李四，李小四) and man(李小四李小四)不確定性匹配是指兩個知識模式不完全一致，但是不確定性

14、匹配是指兩個知識模式不完全一致，但是它們的相似程度又在規(guī)定的限度內(nèi)。它們的相似程度又在規(guī)定的限度內(nèi)。4.1.4 模式匹配變量代換定義4.1 代換是一個形如t1/x1,t2/x2,tn/xn的有限集合。 其中t1,t2,tn是項（常量、變量、函數(shù)）； x1,x2,xn是（某一公式中）互不相同的變元； ti/xi表示用ti代換xi 不允許ti與xi相同，也不允許變元xi循環(huán)地出現(xiàn)在另一個tj中。例如：a/x,f(b)/y,w/z是一個代換g(y)/x,f(x)/y不是代換g(a)/x,f(x)/y是代換令= t1/x1,t2/x2,tn/xn為一個代換，F(xiàn)為表達(dá)式，則F表示對F用ti代換xi后得到

15、的表達(dá)式。F稱為F的特例。 規(guī)則: IF father(x,y) and man(y) THEN son(y,x)事實: father(李四，李小四) and man(李小四) F=father(x,y) man(y) = 李四/X,李小四/Y F= father(李四，李小四) man(李小四) 結(jié)論: son(李小四,李四)代換的復(fù)合定義4.2 設(shè)= t1/x1,t2/x2,tn/xn= u1/y1,u2/y2,um/ym是兩個代換，則這兩個代換的復(fù)合也是一個代換，它是從t1/x1,t2/x2,tn/xn,u1/y1,u2/y2,um/ym中刪去如下兩種元素：ti/xi當(dāng)ti=xiui/y

16、i當(dāng)yix1,x2,xn后剩下的元素所構(gòu)成的集合，記為 。注： ti表示對ti運用進行代換。就是對一個公式F先運用進行代換，然后再運用進行代換：F（ ）=（F ）代換的例子例如，設(shè)有代換= f(y)/x,z/w= a/x,b/y,w/z則=f(y)/x, z/w, a/x, b/y, w/z=f(b)/x, w/w, a/x, b/y, w/z=f(b)/x, b/y, w/z公式集的合一定義4.3 設(shè)有公式集F=F1,F2,Fn，若存在一個代換使得F1=F2=Fn則稱為公式集F的一個合一，且稱F1,F2,Fn是可合一的。例如，設(shè)有公式集F=P(x,y,f(y),P(a,g(x),z)則下式是

17、它的一個合一：=a/x,g(a)/y,f(g(a)/z一個公式集的合一一般不唯一。 最一般的合一定義4.4 設(shè)是公式集F的一個合一，如果對任一個合一都存在一個代換，使得=則稱是一個最一般的合一。（1）代換過程是一個用項代替變元的過程，因此是一個從一般到特殊的過程。（2） 最一般合一是唯一的。求取最一般合一差異集：兩個公式中相同位置處不同符號的集合。例如：F1:P(x,y,z), F2:P(x,f(a),h(b)則D1=y,f(a), D2=z,h(b)求取最一般合一的算法：令k=0,Fk=F, k=。 是空代換。若Fk只含一個表達(dá)式，則算法停止，k就是最一般合一。找出Fk的差異集Dk。若Dk中

18、存在元素xk和tk，其中xk是變元，tk是項，且xk不在tk中出現(xiàn)，則置：Fk+1=Fktk/xkK+1=ktk/xkk=k+1然后轉(zhuǎn)(2)。若不存在這樣的xk和tk則算法停止。1.算法終止，F(xiàn)的最一般合一不存在。求取最一般合一的例子例如，設(shè) F=P(a,x,f(g(y),P(z,f(z),f(u)求其最一般合一。令F0=F, 0=。 F0中有兩個表達(dá)式，所以0不是最一般合一。差異集：D0=a,z。代換： a/zF1= F0 a/z=P(a,x,f(g(y),P(a,f(a),f(u) 。 1=0a/z=a/zD1=x,f(a) 。代換： f(a)/xF2=F1f(a)/x=P(a,f(a),

19、f(g(y),P(a,f(a),f(u) 。 2=1f(a)/x=a/z,f(a)/x D2=g(y),u 。代換： g(y)/uF3=F2g(y)/u=P(a,f(a),f(g(y),P(a,f(a),f(g(y) 。 3=2g(y)/u=a/z,f(a)/x,g(y)/u 4.1.5 沖突消解策略沖突：多個知識都匹配成功。正向推理：n多條產(chǎn)生式前件都與已知事實匹配成功逆向推理：n多條規(guī)則后件都和同一個假設(shè)匹配成功沖突消解的基本思想都是對知識進行排序。幾種沖突消解策略按針對性排序優(yōu)先選用針對性強的產(chǎn)生式規(guī)則。按已知事實的新鮮性排序優(yōu)先選用與較多新事實匹配的規(guī)則。按匹配度排序在不確定性匹配中，

20、計算兩個知識模式的相似度(匹配度)，并對其排序，相似度高的規(guī)則先推。按領(lǐng)域問題特點排序按上下文限制排序把規(guī)則按照下上文分組，并只能選取組中的規(guī)則。按冗余限制排序冗余知識越少的規(guī)則先推。按條件個數(shù)排序條件少的規(guī)則先推。4.2 自然演繹推理從一組已知為真的事實出發(fā)，直接運用經(jīng)典邏輯的推理規(guī)則推出結(jié)論的過程，稱為自然演繹推理。其中，基本的推理規(guī)則是P規(guī)則、T規(guī)則、假言推理、拒取式推理等。假言推理的一般形式拒取式推理的一般形式,P PQQ ,PQQP P規(guī)則：在推理的任何步驟都可以引入前提。T規(guī)則：推理時，如果前面步驟中有一個或者多個公式永真蘊含公式S，則可把S引入推理過程中。4.3 歸結(jié)演繹推理定理

21、證明即證明PQ(PQ)的永真性。根據(jù)反證法，只要證明其否定(PQ) 不可滿足性即可。海伯倫(Herbrand)定理為自動定理證明奠定了理論基礎(chǔ)；魯濱遜(Robinson)提出的歸結(jié)原理使機器定理證明成為現(xiàn)實。4.3.1 子句w在謂詞邏輯中，把原子謂詞公式及其否定統(tǒng)稱為文字。如：P(x)， P(x,f(x)， Q(x,g(x)定義4.5： 任何文字的析取式稱為子句。 例如： P(x)Q(x), P(x,f(x)Q(x,g(x)定義4.6： 不包含任何文字的子句稱為空子句。 子句集(1) 合取范式：C1 C2 C3 Cn(2) 子句集: S= C1 ,C2 ,C3 ,Cn(3)任何謂詞公式F都可通

22、過等價關(guān)系及推理規(guī)則化為相應(yīng)的子句集S。把謂詞公式化成子句集的步驟(1)1. 利用等價關(guān)系消去“”和“”例如公式可等價變換成2. 利用等價關(guān)系把“”移到緊靠謂詞的位置上上式經(jīng)等價變換后3. 重新命名變元，使不同量詞約束的變元有不同的名字上式經(jīng)變換后()() ( , )()( ( , )( , )xy P x yy Q x yR x y ()( () ( , )()( , )( , )xy P x yyQ x yR x y ()()( , ) ()( ( , )( , )xyP x yy Q x yR x y ()()( , ) ()( ( , )( , )xyP x yz Q x zR x z

23、 把謂詞公式化成子句集的步驟(2)4. 消去存在量詞a.存在量詞不出現(xiàn)在全稱量詞的轄域內(nèi)，則只要用一個新的個體常量替換受該量詞約束的變元。b.存在量詞位于一個或者多個全稱量詞的轄域內(nèi)，此時要用Skolem函數(shù)f(x1,x2,xn)替換受該存在量詞約束的變元。上式中存在量詞(y)及(z)都位于(x)的轄域內(nèi)，所以需要用Skolem函數(shù)替換，設(shè)替換y和z的Skolem函數(shù)分別是f(x)和g(x)，則替換后得到5. 把全稱量詞全部移到公式的左邊()( , ( ) ( ( , ( )( , ( )xP x f xQ x g xR x g x()()( , ) ()( ( , )( , )xyP x y

24、z Q x zR x z 把謂詞公式化成子句集的步驟(3)6. 利用等價關(guān)系把公式化為Skolem標(biāo)準(zhǔn)形Skolem標(biāo)準(zhǔn)形的一般形式是其中，M是子句的合取式，稱為Skolem標(biāo)準(zhǔn)形的母式。上式化為Skolem標(biāo)準(zhǔn)形后得到7. 消去全稱量詞8. 對變元更名，使不同子句中的變元不同名上式化為9. 消去合取詞，就得到子句集()() ()PQ RP QP R12()()()nxxx M()( , ( )( , ( ) ( , ( )( , ( )xP x f xQ x g xP x f xR x g x ( , ( )( , ( ) ( , ( )( , ( )P x f xQ x g xP y f

25、yR y g y ( , ( )( , ( )( , ( )( , ( )P x f xQ x g xP y f yR y g y 子句集的性質(zhì)（1）子句集中子句之間是合取關(guān)系。（2）子句集中的變元受全稱量詞的約束。 子句集的意義子句集S的不可滿足性：對于任意論域中的任意一個解釋，S中的子句不能同時取得真值T。定理4.1 設(shè)有謂詞公式F，其子句集為S，則F不可滿足的充要條件是S不可滿足。要證明PQ永真，只需證明公式F=(PQ)永假，即S不可滿足。4.3.2 Herbrand理論為了判斷子句集的不可滿足性，需要對所有可能論域上的所有解釋進行判定。只有當(dāng)子句集對任何非空個體域上的任何一個解釋都是不

26、可滿足的，才可斷定該子句集是不可滿足的。海伯倫構(gòu)造了一個特殊的論域(海伯倫域)，并證明只要對這個特殊域上的一切解釋進行判定，就可知子句集是否不可滿足。海伯倫域定義4.7 設(shè)S為子句集，則按下述方法構(gòu)造的域H稱為海伯倫域，記為H域。(1)令H0是S中所有個體常量的集合，若S中不包含個體常量，則令H0a，其中a為任意指定的一個個體常量。(2)令Hi+1=HiS中所有n元函數(shù)f(x1,xn)|xj(j=1,n)是Hi中的元素，其中i=0,1,2,。例4.3 求子句集S=P(x)Q(x),R(f(y)的H域。解：此例中沒有個體常量，任意指定一個常量a作為個體常量，得到H0=aH1=a,f(a)H2=a

27、,f(a),f(f(a)H3=a,f(a),f(f(a),f(f(f(a)H=a,f(a),f(f(a),f(f(f(a),為研究子句集的永假性，引入H域上的原子謂詞公式實例集A:A=所有出現(xiàn)于S中原子謂詞公式的實例n若原子公式是命題（不包含變量），則其實例就是其本身；n若原子公式形如P(t1, t2, tm), ti是變量（i=1，2，m）,則其實例通過讓ti=kiH(即H)來形成（i=1，2，m）。例如，對于上述例4.3，有： A=P(a), Q(f(a), Q(f(f(a),我們稱A中的元素為基原子，進而A也稱為基原子集。鑒于這些元素都是原子命題，只要給它們每個指派一個真值（T或F），就

28、可建立子句集在H域上的一個解釋，記為I*。就以基原子自身指示取真值T，前面加取反符號指示取真值F, 則對于上述第一例，有 I*1 = P(a), Q(f(a), Q(f(f(a), I*2 = P(a), Q(f(a), Q(f(f(a), 一個子句集的基原子有無限多個，它在一個子句集的基原子有無限多個，它在H域上的解域上的解釋也有無限多個。釋也有無限多個。在H域上進行解釋的意義意義：對于S任意可能論域D上的任意一個解釋I，總存在H域上的一個解釋I與它對應(yīng)，且子句集在這兩個解釋下具有相同的真值。定理4.2 子句集S不可滿足的充要條件是S對H域上一切解釋都為假。4.3.3 魯濱遜歸結(jié)原理 魯濱遜

29、歸結(jié)原理的基本思想：檢查子句集S中是否包含空子句。若包含，則S不可滿足；若不包含，就在子句集中選擇合適的子句進行歸結(jié)，一旦通過歸結(jié)能推出空子句，就說明子句集S是不可滿足的。 子句集S的不可滿足性：對于任意論域中的任意一個解釋，S中的子句不能同時取得真值T。一旦S中包含空子句，則S必不可滿足。命題邏輯中的歸結(jié)原理定義4.9 若P是原子謂詞公式，則稱P與P為互補文字。在命題邏輯中，P為命題。定義4.10 設(shè)C1與C2是子句集中的任意兩個子句。如果C1中的文字L1與C2中文字L2互補，那么從C1和C2中分別消去L1和L2，并將兩個子句中余下的部分析取，構(gòu)成一個新子句C12，則稱這一過程為歸結(jié)。稱C1

30、2為C1和C2的歸結(jié)式，C1和C2為C12的親本子句。例4.9 設(shè)C1=PQ, C2=QR, C3=PC1與C2歸結(jié)得到：C12=PRC12與C3歸結(jié)得到：C123=R定理4.4 C12是其親本子句C1與C2的邏輯結(jié)論。證明：設(shè)C1=LC1, C2=LC2, 則C12=C1C2111222() ()1212() ()12121212121212CCLCLCL CLCCCCLLCCLLCCCCCCCCCCC 由假言三段論推論1 設(shè)C1與C2是子句集S中的兩個子句，C12是它們的歸結(jié)式。若用C12代替C1和C2后得到新子句集S1，則由S1的不可滿足性可推出原子句集S的不可滿足性，即S1的不可滿足性

31、S的不可滿足性推論2 設(shè)C1與C2是子句集S中的兩個子句，C12是它們的歸結(jié)式。若把C12加入S中得到新子句集S2，則S與S2在不可滿足的意義上是等價的，即S2的不可滿足性S的不可滿足性推論1及推論2保證了我們可以用歸結(jié)的方法來證明子句集S的不可滿足性。為了要證明子句集S的不可滿足性，只要對其中可進行歸結(jié)的子句進行歸結(jié)，并把歸結(jié)式加入子句集S，或者用歸結(jié)式替換它的親本子句，然后對新子句集(S1或者S2)證明不可滿足性就可以了。如果經(jīng)過歸結(jié)能得到空子句，則立即可得原子句集S是不可滿足的結(jié)論。在命題邏輯中，對不可滿足的子句集S，歸結(jié)原理是完備的。即，若子句集不可滿足，則必然存在一個從S到空子句的歸

32、結(jié)演繹；若存在一個從S到空子句的歸結(jié)演繹，則S一定是不可滿足的。謂詞邏輯中的歸結(jié)原理在謂詞邏輯中，由于子句中含有變元，所以不能像命題邏輯那樣直接消去互補文字，而需要先用最一般合一對變元進行代換，然后才能進行歸結(jié)。例如,設(shè)有兩個子句C1=P(x)Q(x), C2= P(a)R(y)由于P(x)與P(a)不同，所以C1與C2不能直接進行歸結(jié)。但是若用最一般合一=a/x對兩個子句分別進行代換：C1 =P(a)Q(a)C2 = P(a)R(y)就可對它們進行歸結(jié)，得到歸結(jié)式：Q(a)R(y)二元歸結(jié)式的定義定義4.11 設(shè)C1與C2是兩個沒有相同變元的子句，L1和L2分別是C1和C2中的文字。若是L1

33、和L2的最一般合一，則稱C12=(C1-L1)(C2-L2)為C1和C2的二元歸結(jié)式，L1和L2稱為歸結(jié)式上的文字。例4.10 設(shè)C1=P(a)Q(x)R(x), C2=P(y)Q(b)若選L1=P(a),L2=P(y)，則有：L1=P(a), L2=P(y)，=a/y就是L1與L2的最一般合一?？傻茫篊12=(C1-L1)(C2-L2)= Q(x)R(x)Q(b)若子句C含有可合一的文字，則在進行歸結(jié)之前應(yīng)先對這些文字進行合一。記其最一般的合一為，稱C子句C的因子。 C1=P(x)VP(f(a)VQ(x), C2= P(y) VR(b) = f(a)/x C1=P(f(a) VQ(f(a)

34、C12 = Q(f(a) VR(b) 定義4.12 子句C1和C2的歸結(jié)式是下列二元歸結(jié)式之一：nC1與C2的二元歸結(jié)式；nC1與C2的因子C22的二元歸結(jié)式；nC1的因子C11與C2的二元歸結(jié)式；nC1的因子C11與C2的因子C22的二元歸結(jié)式。對于一階謂詞邏輯歸結(jié)原理也是完備的。即，若子句集S不可滿足，則必然存在一個從S到空子句的歸結(jié)演繹；若存在一個從S到空子句的歸結(jié)演繹，則S一定是不可滿足的。4.3.4 歸結(jié)反演如欲證明Q為P1,P2,Pn的邏輯結(jié)論，只需證(P1P2Pn)Q是不可滿足的，或證明其子句集是不可滿足的。而子句集的不可滿足性可用歸結(jié)原理來證明。應(yīng)用歸結(jié)原理證明定理的過程稱為歸

35、結(jié)反演。設(shè)F為已知前提的公式集，Q為目標(biāo)公式(結(jié)論)，用歸結(jié)反演證明Q為真的步驟是：否定Q，得到Q；把Q并入到公式集F中，得到F, Q;把公式集F, Q化為子句集S；1.應(yīng)用歸結(jié)原理對子句集S中的子句進行歸結(jié)，并把每次歸結(jié)得到的歸結(jié)式都并入S中。如此反復(fù)進行，若出現(xiàn)了空子句，則停止歸結(jié)，此時就證明了Q為真。歸結(jié)反演的例子例4.12 已知求證：G是F的邏輯結(jié)論。證明：首先把F和G化為子句集：然后進行歸結(jié)：(6)A(x,y)B(y)由(1)與(3)歸結(jié)，f(x)/z(7)B(b)由(4)與(6)歸結(jié)，a/x,b/y(8)NIL由(5)與(7)歸結(jié)所以G是F的邏輯結(jié)論。上述歸結(jié)過程如右圖歸結(jié)樹所示。

36、: ()()( ( , )( )()( ( )( , ):() ( )()()( ( , )( )Fxy A x yB yy C yD x yGx C xxy A x yB y ( , )( )( ( ),( , )( )( , ( )( ), ( , ), ( )FA x yB yC f xA x yB yD x f xGC zA a b B b A(x,y)B(y)C(f(x)A(x,y)B(y)B(b)NILC(z)A(a,b)B(b)假設(shè)：所有不貧窮并且聰明的人都是快樂的，那些看書的人是聰明的。李明能看書且不貧窮，快樂的人過著激動人心的生活。求證：李明過著激動人心的生活。解：先定義謂詞

37、： Poor(x) x是貧窮的 Smart(x) x是聰明的 Happy(x) x是快樂的 Read(x) x能看書 Exciting(x) x過著激動人心的生活問題謂詞表示：n “所有不貧窮并且聰明的人都是快樂的” (x)(Poor(x)Smart(x)Happy(x)n“那些看書的人是聰明的” (y) (Read(y) Smart(y)n“李明能看書且不貧窮” Read(Liming)Poor(Liming)n“快樂的人過著激動人心的生活” (z) (Happy(z)Exciting(z)n目標(biāo)“李明過著激動人心的生活”的否定 Exciting(Liming)將上述謂詞公式轉(zhuǎn)化為子句集如下

38、： (1) Poor(x)Smart(x)Happy(x) (2) Read(y)Smart(y) (3) Read(Liming) (4) Poor(Liming) (5) Happy(z)Exciting(z) (6) Exciting(Liming) (結(jié)論的否定) Exciting(Liming) Happy(z)Exciting(z)Happy(Liming)Happy(x)Smart(x)Happy(x)Poor(Liming)Smart(Liming)Read(y)Smart(y )Poor(Liming)Read(Liming)Poor(Liming)Read(Liming)R

39、ead(Liming) NILLiming/zLiming/xLiming/y4.3.5 應(yīng)用歸結(jié)原理求取問題的答案求解的步驟：把已知前提用謂詞公式表示出來，并且化為相應(yīng)的子句集。設(shè)該子句集的名字為S。把待求解的問題也用謂詞公式表示出來，然后把它否定并與謂詞Answer構(gòu)成析取式。Answer是一個為了求解問題而專設(shè)的謂詞。把此析取式化為子句集，并且把該子句集并入到子句集S中，得到子句集S。對S應(yīng)用歸結(jié)原理進行歸結(jié)。1.若得到歸結(jié)式Answer，則答案就在Answer中。用歸結(jié)原理求解問題的例子(1)例4.16 設(shè)A,B,C三人中有人從不說真話，也有人從不說假話。某人向這三人分別提出同一個問題

40、：誰是說謊者？A答：“B和C都是說謊者”；B答：“A和C都是說謊者”；C答：“A和B中至少有一個是說謊者”。求誰是老實人，誰是說謊者？解：設(shè)用T(x)表示x說真話。 T(C)T(A)T(B) T(C)T(A)T(B) T(A)T(B)T(C) T(A)T(B)T(C) T(B)T(A)T(C) T(B)T(A)T(C) T(C)T(A)T(B) T(C)T(A)T(B)用歸結(jié)原理求解問題的例子(2)把上述公式化成子句集，得到S：(1)T(A)T(B)(2)T(A)T(C)(3)T(C)T(A)T(B)(4)T(B)T(C)(5)T(C)T(A)T(B)(6) T(A)T(C)(7)T(B)T(

41、C)下面先求誰是老實人。把T(x)Ansewer(x)并入S得到S1。即多一個子句：(8)T(x)Ansewer(x)應(yīng)用歸結(jié)原理對S1進行歸結(jié)：(9)T(A)T(C)(1)和(7)歸結(jié)(10)T(C) (6)和(9)歸結(jié)(11)Ansewer(C) (8)和(10)歸結(jié)所以C是老實人，即C從不說假話。(1)T(A)T(B)(2)T(A)T(C)(3)T(C)T(A)T(B)(4)T(B)T(C)(5)T(C)T(A)T(B)(6) T(A)T(C)(7)T(B)T(C)下面證明A不是老實人，即證明T(A)。對T(A)進行否定，并入S中，得到子句集S2，即S2比S多如下子句：(8)(T(A),

42、 即T(A)應(yīng)用歸結(jié)原理對S2進行歸結(jié)：(9)T(A)T(C) (1)和(7)歸結(jié)(10)T(A) (2)和(9)歸結(jié)(11)NIL (8)和(10)歸結(jié)所以A不是老實人。同樣可以證明B也不是老實人。歸結(jié)時，并不要求把子句集中所有的子句都用到。在歸結(jié)過程中，一個子句可以多次被用來進行歸結(jié)。4.3.6 歸結(jié)策略歸結(jié)策略可分為兩大類：一類是刪除策略；刪除某些無用的子句來縮小歸結(jié)的范圍。一類是限制策略。通過對參加歸結(jié)的子句進行種種限制，盡可能減小歸結(jié)的盲目性，使其盡快地歸結(jié)出空子句。歸結(jié)的一般過程設(shè)有子句集S=C1,C2,C3,C4，則對此子句集歸結(jié)的一般過程是：S內(nèi)任意子句兩兩逐一進行歸結(jié)，得到一

43、組歸結(jié)式，稱為第一級歸結(jié)式，記為S1。把S與S1內(nèi)的任意子句兩兩逐一進行歸結(jié)，得到一組歸結(jié)式，稱為第二級歸結(jié)式，記為S2。S和S1內(nèi)的子句與S2內(nèi)的任意子句兩兩逐一進行歸結(jié)，得到一組歸結(jié)式，稱為第三級歸結(jié)式，記為S3。如此繼續(xù)，直到出現(xiàn)了空子句或者不能再繼續(xù)歸結(jié)為止。一個歸結(jié)的例子例4.17 設(shè)有子句集S=P, R,PQ,QR。歸結(jié)過程為：S: (1)P(2)R(3)PQ(4)QRS1: (5)Q (1)與(3)歸結(jié)(6)Q (2)與(4)歸結(jié)(7)PR (3)與(4)歸結(jié)S2: (8)R (1)與(7)歸結(jié)(9)P (2)與(7)歸結(jié)(10)P (3)與(6)歸結(jié)(11)R (4)與(5)歸

44、結(jié)S3: (12) NIL (1)與(9)歸結(jié)刪除策略純文字刪除法如果某文字L在子句集中不存在可與之互補的文字L，則稱該文字為純文字。包含純文字的子句可以刪除。重言式刪除法如果一個子句中同時包含互補文字對，則該字句稱為重言式。重言式是永遠(yuǎn)為真的子句，可以刪除。支持集策略對參加歸結(jié)的子句提出如下限制：每一次歸結(jié)時，親本子句中至少有一個是由目標(biāo)公式的否定所得到的子句，或者是它的后裔。可以證明，支持集策略是完備的。例4.18 設(shè)有子句集S=I(x)R(x),I(a),R(y)L(y),L(a)其中I(x)R(x)是目標(biāo)公式否定后得到的子句。用支持集策略進行歸結(jié)的過程是：S:(1) I(x)R(x)(

45、2) I(a)(3) R(y)L(y)(4) L(a)S1:(5) R(a) (1)與(2)歸結(jié)(6) I(x)L(x) (1)與(3)歸結(jié)S2:(7) L(a) (2)與(6)歸結(jié)(8) L(a) (3)與(5)歸結(jié)(9) I(a) (4)與(6)歸結(jié)S3:(10)NIL (2)與(9)歸結(jié)支持集策略示例I(x)R(x)I(a)R(y)L(y)L(a)R(a)L(a)I(x)L(x)L(a)I(a)NIL12345678910線性輸入策略限制：參加歸結(jié)的兩個子句中必須至少有一個是初始子句集中的子句。線性輸入策略可限制生成歸結(jié)式的數(shù)量，具有簡單、高效的優(yōu)點。但是它是不完備的。I(x)R(x)I

46、(a)R(y)L(y)L(a)R(a)L(a)I(x)L(x)L(a)I(a)NIL123456981112R(a)I(a)710單文字子句策略如果一個子句只包含一個文字，則稱它為單文字子句。限制：參加歸結(jié)的兩個子句中必須至少有一個是單文字子句。用單文字子句策略歸結(jié)時，歸結(jié)式比親本子句含有較少的文字，這有利于朝著空子句的方向前進，因此它有較高的歸結(jié)效率。但是，這種歸結(jié)策略是不完備的。當(dāng)初始子句集中不包含單文字子句時，歸結(jié)就無法進行。祖先過濾策略該策略與線性策略比較相似，但放寬了限制。當(dāng)對兩個子句C1和C2進行歸結(jié)時，只要它們滿足下述任一個條件就可以歸結(jié)。C1和C2中至少有一個是初始子句集中的子

47、句。C1和C2中一個是另外一個的祖先子句。1.祖先過濾策略是完備的。優(yōu)點：簡單，便于在計算機上實現(xiàn)。缺點：必須把邏輯公式化成子句集。不便于閱讀與理解。P(x)Q(x)沒有P(x)Q(x)直觀?？赡軄G失控制信息。下列邏輯公式：(AB)C A(BC)(AC)B B(AC)(CB)A C(BA)化成子句后都是: ABC歸結(jié)演繹推理的特點4.4 與/或形演繹推理歸結(jié)演繹推理要求把有關(guān)問題的知識及目標(biāo)的否定都化成子句形式，然后通過歸結(jié)進行演繹推理，其推理規(guī)則只有一條，即歸結(jié)規(guī)則；與/或形演繹推理不再把有關(guān)知識轉(zhuǎn)化成子句集，而把領(lǐng)域知識及已知事實分別用蘊含式及與/或形表示出來，然后通過運用蘊含式進行演繹推

48、理，從而證明某個目標(biāo)公式?；谝?guī)則的演繹推理規(guī)則規(guī)則是一種比較接近于人們習(xí)慣的問題描述方式是一種比較接近于人們習(xí)慣的問題描述方式，用蘊含式（，用蘊含式（“If Then”規(guī)則）按照這種問題描規(guī)則）按照這種問題描述方式進行求解的系統(tǒng)稱為述方式進行求解的系統(tǒng)稱為基于規(guī)則的系統(tǒng)基于規(guī)則的系統(tǒng)，或，或者叫做者叫做規(guī)則演繹系統(tǒng)規(guī)則演繹系統(tǒng)。規(guī)則正向演繹系統(tǒng)規(guī)則正向演繹系統(tǒng)規(guī)則逆向演繹系統(tǒng)規(guī)則逆向演繹系統(tǒng)規(guī)則雙向演繹系統(tǒng)規(guī)則雙向演繹系統(tǒng)規(guī)則正向演繹系統(tǒng)規(guī)則正向演繹系統(tǒng)是從已知事實出發(fā)，正向使規(guī)則正向演繹系統(tǒng)是從已知事實出發(fā)，正向使用規(guī)則（蘊含式）直接進行演繹，直至到達(dá)目用規(guī)則（蘊含式）直接進行演繹，直至到

49、達(dá)目標(biāo)為止。標(biāo)為止。在規(guī)則正向演繹系統(tǒng)中，對已知在規(guī)則正向演繹系統(tǒng)中，對已知事實事實和和規(guī)則規(guī)則都都有一定的要求，如果不是所要求的形式，需要有一定的要求，如果不是所要求的形式，需要進行變換。進行變換。在基于規(guī)則的正向演繹系統(tǒng)中，把在基于規(guī)則的正向演繹系統(tǒng)中，把事實事實表示為表示為非蘊含形式非蘊含形式的的與與或形或形，作為系統(tǒng)的總數(shù)據(jù)庫，作為系統(tǒng)的總數(shù)據(jù)庫把一個公式化為與或形的步驟與化為子句集類似，把一個公式化為與或形的步驟與化為子句集類似，只是不必把只是不必把公式化為子句的合取形式，也不能消去公式中的合取。公式化為子句的合取形式，也不能消去公式中的合取。規(guī)則正向演繹系統(tǒng)(1) 利用利用 “PQ

50、PQ”，消去蘊含符號；，消去蘊含符號； (2) 利用狄利用狄.摩根定律及量詞轉(zhuǎn)換率把摩根定律及量詞轉(zhuǎn)換率把“”移到緊靠謂詞的位移到緊靠謂詞的位置，直到否定符號的轄域最多只含一個謂詞為止；置，直到否定符號的轄域最多只含一個謂詞為止；(3)重新命名變元，使重新命名變元，使不同量詞約束的變元有不同的名字不同量詞約束的變元有不同的名字；(4)對存在量詞量化的變量用對存在量詞量化的變量用skolem函數(shù)代替；函數(shù)代替；(5) 消去全稱量詞，且消去全稱量詞，且使各主要合取式中的變元具有不同的變使各主要合取式中的變元具有不同的變量名量名。規(guī)則正向演繹系統(tǒng)有如下表達(dá)式有如下表達(dá)式 (x) (y)(Q(y, x

51、)(R(y)P(y)S(x, y)可把它轉(zhuǎn)化為：可把它轉(zhuǎn)化為： Q(z, a)( ( R(y)P(y) )S(a, y) )這就是這就是與與/或形表示或形表示。事實表達(dá)式的事實表達(dá)式的與與/或形或形可用一棵可用一棵與與/或圖或圖表示出來。表示出來。規(guī)則正向演繹系統(tǒng)Q(z, a)(R(y)P(y)S(a, y)的與的與/或圖表示或圖表示如下：如下：w Q(z, a)(R(y)P(y)S(a, y)wQ(z, a)w(R(y)P(y)S(a, y)wR(y)P(y)w S(a, y)wR(y)wP(y)規(guī)則正向演繹系統(tǒng)當(dāng)某表達(dá)式為當(dāng)某表達(dá)式為k個子表達(dá)式的析取：個子表達(dá)式的析?。篍1E2Ek，其中

52、的每個子表達(dá)式，其中的每個子表達(dá)式Ei均被表示為均被表示為E1E2Ek的的后繼節(jié)點后繼節(jié)點，并由一個，并由一個k線連接符線連接符（即圖中的半圓?。磮D中的半圓?。⑦@些后繼節(jié)點都連接到其父節(jié)點，即）將這些后繼節(jié)點都連接到其父節(jié)點，即表示成與的表示成與的關(guān)系關(guān)系。當(dāng)某表達(dá)式為當(dāng)某表達(dá)式為k個子表達(dá)式的合?。簜€子表達(dá)式的合?。篍1E2Ek，其中的每個子表達(dá)式，其中的每個子表達(dá)式Ei均被表示為均被表示為E1E2Ek的一個單一的后繼節(jié)點，無需用連接符連接，即的一個單一的后繼節(jié)點，無需用連接符連接，即表示表示成或的關(guān)系成或的關(guān)系。這樣，與這樣，與/或圖的或圖的根節(jié)點根節(jié)點就是整個事實表達(dá)式，就是整個事實

53、表達(dá)式，葉節(jié)葉節(jié)點點均為事實表達(dá)式中的一個均為事實表達(dá)式中的一個文字文字。規(guī)則正向演繹系統(tǒng)有了與有了與/或圖的表示，就可以求出其或圖的表示，就可以求出其解樹（結(jié)束于文解樹（結(jié)束于文字節(jié)點上的子樹）集字節(jié)點上的子樹）集。可以發(fā)現(xiàn)，事實表達(dá)式的子句。可以發(fā)現(xiàn)，事實表達(dá)式的子句集與解樹集之間存在著一一對應(yīng)關(guān)系，即集與解樹集之間存在著一一對應(yīng)關(guān)系，即解樹集中的解樹集中的每個解樹都對應(yīng)著子句集中的一個子句每個解樹都對應(yīng)著子句集中的一個子句。解樹集中每個解樹的端節(jié)點上的文字的析取就是子句解樹集中每個解樹的端節(jié)點上的文字的析取就是子句集中的一個子句。集中的一個子句。上圖所示的與上圖所示的與/或圖有或圖有3個

54、解樹，分別對應(yīng)這以個解樹，分別對應(yīng)這以下下3個子句：個子句： Q(z, a) R(y) S(a, y) P(y) S(a, y)規(guī)則正向演繹系統(tǒng)為簡化演繹過程，通常要求規(guī)則具有如下形式：為簡化演繹過程，通常要求規(guī)則具有如下形式： LW其中，其中，L為為單文字單文字，W為為與與/或形公式或形公式。假定出現(xiàn)在蘊含式中的任何變量全都受假定出現(xiàn)在蘊含式中的任何變量全都受全稱量詞的全稱量詞的約束約束，并且這些變量已經(jīng)被換名，使得他們，并且這些變量已經(jīng)被換名，使得他們與事實與事實公式和其他規(guī)則中的變量不同公式和其他規(guī)則中的變量不同。如果領(lǐng)域知識的規(guī)則表示形式與上述要求不同，則如果領(lǐng)域知識的規(guī)則表示形式與上

55、述要求不同，則應(yīng)應(yīng)將它轉(zhuǎn)換成要求的形式。將它轉(zhuǎn)換成要求的形式。規(guī)則正向演繹系統(tǒng)(1) 暫時消去蘊含符號暫時消去蘊含符號“”。設(shè)有如下公式：。設(shè)有如下公式： (x)(y) ( z)P(x, y,z)(u)Q(x, u) 運用等價關(guān)系運用等價關(guān)系“PQPQ”，可將上式變?yōu)椋?，可將上式變?yōu)椋?(x)( y) (z)P(x, y,z)(u)Q(x, u)(2) 把否定符號把否定符號“”移到緊靠謂詞的位置上，使其作移到緊靠謂詞的位置上，使其作用域僅限于單個謂詞。通過使用狄用域僅限于單個謂詞。通過使用狄.摩根定律及量詞轉(zhuǎn)摩根定律及量詞轉(zhuǎn)換率可把上式轉(zhuǎn)換為：換率可把上式轉(zhuǎn)換為： ( x)( (y) (z)P

56、(x, y,z) (u)Q(x, u)規(guī)則正向演繹系統(tǒng)(3) 引入引入Skolem函數(shù)，消去存在量詞。消去存在量函數(shù)，消去存在量詞。消去存在量詞后，上式可變?yōu)椋涸~后，上式可變?yōu)椋?( x)( (y) (P(x, y,f(x,y)(u)Q(x, u)(4)把所有全稱量詞移至前面化成前束式，消去全部把所有全稱量詞移至前面化成前束式，消去全部全稱量詞。消去全稱量詞后，上式變?yōu)椋喝Q量詞。消去全稱量詞后，上式變?yōu)椋?P(x, y,f(x,y)Q(x, u) 此公式中的變元都被視為受全稱量詞約束的變元。此公式中的變元都被視為受全稱量詞約束的變元。(5) 恢復(fù)蘊含式表示。利用等價關(guān)系恢復(fù)蘊含式表示。利用等

57、價關(guān)系“PQPQ”將上式變?yōu)椋簩⑸鲜阶優(yōu)椋?P(x, y,f(x,y)Q(x, u)規(guī)則正向演繹系統(tǒng)在上述對規(guī)則的要求中，在上述對規(guī)則的要求中，之所以限制其前件為單文字之所以限制其前件為單文字，是因為，是因為在進行正向演繹推理時要用規(guī)則作用于表示在進行正向演繹推理時要用規(guī)則作用于表示事實的與事實的與/或樹，而該與或樹，而該與/或樹的葉節(jié)點都是單文字，這或樹的葉節(jié)點都是單文字，這樣就可用規(guī)則的前件與葉節(jié)點進行簡單匹配。樣就可用規(guī)則的前件與葉節(jié)點進行簡單匹配。對非單文字情況，若形式為對非單文字情況，若形式為L1L2W，則可將其轉(zhuǎn)，則可將其轉(zhuǎn)換成與之等價的兩個規(guī)則換成與之等價的兩個規(guī)則L1W與與 L

58、2W進行處理。進行處理。與與/或樹正向演繹系統(tǒng)要求目標(biāo)公式用或樹正向演繹系統(tǒng)要求目標(biāo)公式用子句形子句形表示。表示。如果目標(biāo)公式不是子句形，則需要化成子句形。如果目標(biāo)公式不是子句形，則需要化成子句形。規(guī)則正向演繹系統(tǒng)規(guī)則正向演繹推理過程是從已知事實出發(fā)，不斷運規(guī)則正向演繹推理過程是從已知事實出發(fā)，不斷運用規(guī)則，推出欲證明目標(biāo)公式的過程。用規(guī)則，推出欲證明目標(biāo)公式的過程。先用與先用與/或樹把已知事實表示出來，然后再用規(guī)則的或樹把已知事實表示出來，然后再用規(guī)則的前件和與前件和與/或樹的或樹的葉節(jié)點進行匹配葉節(jié)點進行匹配，并通過一個匹配，并通過一個匹配弧把匹配成功的規(guī)則加入到與弧把匹配成功的規(guī)則加入到

59、與/或樹中，依此使用規(guī)或樹中，依此使用規(guī)則，直到產(chǎn)生一個含有則，直到產(chǎn)生一個含有以目標(biāo)節(jié)點為終止節(jié)點以目標(biāo)節(jié)點為終止節(jié)點的解的解樹為止。樹為止。下面分下面分命題邏輯命題邏輯和和謂詞邏輯謂詞邏輯兩種情況來討論規(guī)則正兩種情況來討論規(guī)則正向演繹過程。向演繹過程。規(guī)則正向演繹系統(tǒng)已知事實：已知事實：AB規(guī)則：規(guī)則： r1: ACD r2: BEG目標(biāo)公式：目標(biāo)公式：CG證明：證明：1）先將已知事實用與）先將已知事實用與/或樹表示出來；或樹表示出來；2）然）然后再用匹配弧把后再用匹配弧把r1和和r2分別連接到事實與分別連接到事實與/或樹中與或樹中與r1和和r2 的前件匹配的兩個不同端節(jié)點；的前件匹配的兩

60、個不同端節(jié)點；3 ) 由于出由于出現(xiàn)了現(xiàn)了以目標(biāo)節(jié)點為終節(jié)點的解樹以目標(biāo)節(jié)點為終節(jié)點的解樹，故推理過程結(jié)束，故推理過程結(jié)束。這一證明過程可用下圖表示。這一證明過程可用下圖表示。規(guī)則正向演繹系統(tǒng)在該圖中，雙箭頭表示匹配弧，它相當(dāng)于一個單線在該圖中，雙箭頭表示匹配弧，它相當(dāng)于一個單線連接符。連接符。C GCD E G A B A B ABw目標(biāo)目標(biāo)w匹配匹配w匹配匹配w規(guī)則規(guī)則w已知事實已知事實 r1 r2規(guī)則正向演繹系統(tǒng)已知事實的與已知事實的與/或形表示：或形表示：P(x, y)(Q(z)R(v, y)規(guī)則：規(guī)則： P(u, v)(S(u)N(v) 目標(biāo)公式：目標(biāo)公式： S(a)N(b)Q(c)