吉林大學(xué)研究生人工智能t演示文檔

《吉林大學(xué)研究生人工智能t演示文檔》由會(huì)員分享，可在線閱讀，更多相關(guān)《吉林大學(xué)研究生人工智能t演示文檔（127頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

.,6/27/2018,1,第六章 歸結(jié)原理,6.1 子句集的Herbrand域 一、 Herbrand域與 Herbrand解釋 定義（Herbrand域）設(shè)S為子句集，令H0是出現(xiàn)于子句集S的常量符號(hào)集。如果S中無(wú)常量符號(hào)出現(xiàn)，則H0由一個(gè)常量符號(hào)a組成。 對(duì)于i＝1，2，…，令 Hi = Hi-1?｛所有形如f(t1，…，tn)的項(xiàng)｝ 其中f(t1，…，tn)是出現(xiàn)在S中的所有n元函數(shù)符號(hào)， tj? Hi-1，j＝1，…，n． 稱(chēng)Hi為S的i級(jí)常量集，H? 稱(chēng)為S的Herbrand域， 簡(jiǎn)稱(chēng)S的H域。,.,6/27/2018,2,,例 S＝｛P(f(x)，a，g(y)，b)｝ H0 ={a, b} H1 ={a, b, f(a), f(b), g(a), g(b)} H2＝{a, b, f(a), f(b), g(a), g(b), f(f(a)), f(f(b)), f(g(a)), f(g(b)), g(f(a)), g(f(b)), g(g(a)), g(g(b))} …,.,6/27/2018,3,練習(xí): 求S的Herbrand域,S＝{P(x) ? Q(y)，R(z) } S＝{Q(a) ?～P(f(x))， ～Q(b) ? P(g(x,y)) },.,6/27/2018,4,原子集 基例,基：把對(duì)象中的變量用常量代替后得到的無(wú)變量符號(hào)出現(xiàn)的對(duì)象。 基項(xiàng)、基項(xiàng)集、基原子、基原子集合、基文字、基子句、基子句集 定義 (原子集、Herbrand底) 設(shè)S是子句集，形如P(t1,…,tn)的基原子集合，稱(chēng)為S的Herbrand底或S的原子集． 其中P(x1，…，xn)是出現(xiàn)于S的所有n元謂詞符號(hào)，t1，…，tn是S的H域中的元素． 定義（基例） 設(shè)S是子句集，C是S中的一個(gè)子句．用S的H域中元素代替C中所有變量所得到的基子句稱(chēng)為子句C的基例。,.,6/27/2018,5,練習(xí),已知S＝｛P(f(x)，a，g(y)，b)｝，求S的原子集， 給出P(f(x)，a，g(y)，b)的一個(gè)基例。 已知S＝{P(x) ? Q(y)，R(z) }，求S的原子集， 分別給出P(x) ? Q(y)， R(z)的所有基例。 已知S＝ {Q(a)?～P(f(x))，～Q(b)? P(g(x,y))}， 求S的原子集， 分別給出Q(a)?～P(f(x)) ， ～Q(b)? P(g(x,y))的一個(gè)基例。 設(shè)S＝{P(x), Q(f(y)) ? R(y) }，求S的H域， S的原子集， P(x)的基例, Q(f(y)) ? R(y) 的基例。,.,6/27/2018,6,H解釋,定義（子句集的H解釋?zhuān)? 設(shè)S是子句集，H是S的H域，I*是S在H上的一個(gè)解釋?zhuān)Q(chēng)I*為S的一個(gè)H解釋?zhuān)绻鸌*滿足如下條件： 1） I*映射S中的所有常量符號(hào)到自身。 2）若f是S中n元函數(shù)符號(hào)，h1，…，hn是H中元素，則I*指定映射： (h1，…，hn) ?f (h1，…，hn) 設(shè)A={A1，A2，…，An， … } 是S的原子集。于是S的一個(gè)H解釋I可方便地表示為如下一個(gè)集合： I* ＝｛m1，m2，…，mn，…｝ 其中, mi =,,,.,6/27/2018,7,H解釋的例子,例 S={P(x)?Q(x), R(f(y)) } S的H域={a, f(a), f(f(a)), … } S的原子集： A={P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), … } S的H解釋?zhuān)? I1* ={ P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), … } I2* ={ ～P(a), ～Q(a), R(a), P(f(a)), ～Q(f(a)), ～R(f(a)), … },.,6/27/2018,8,練習(xí),S={P(x)?Q(x), ～P(a), ～Q(b) }， 求S的所有H解釋。,.,6/27/2018,9,二、Herbrand解釋與普通解釋的關(guān)系,子句集S的H解釋是S的普通解釋。 S的普通解釋不一定是S的H解釋?zhuān)浩胀ń忉尣皇潜仨毝x在H域上，即使定義在H域上，也不一定是一個(gè)H解釋。 任取普通解釋I，依照I，可以按如下方法構(gòu)造S的一個(gè)H解釋I*，使得若 S在 I下為真則 S在I*下也為真。,.,6/27/2018,10,例.,S＝｛P(x), Q(y,f(y,a))｝ 令S的一個(gè)解釋I如下： D＝{1，2} a f(1, 1) f(1, 2) f(2, 1) f(2, 2) 2 1 2 2 1 P(1) P(2) Q(1, 1) Q(1, 2) Q(2, 1) Q(2, 2) T F F T F T 對(duì)應(yīng)于I的H解釋I*： I*＝｛～P(a), Q(a, a), P(f(a, a)), ～Q(a, f(a, a)), Q(f(a, a), a), ～Q(f(a, a), f(a, a)), …｝,.,6/27/2018,11,例,S={P(x), Q(y, f(y, z))} 令S的一個(gè)解釋I如下: D={1, 2} f(1, 1) f(1, 2) f(2, 1) f(2, 2) 1 2 2 1 P(1) P(2) Q(1, 1) Q(1, 2) Q(2, 1) Q(2, 2) T F F T F T 指定 a對(duì)應(yīng)1得H解釋?zhuān)?I1*＝｛P(a), ～Q(a, a), P(f(a, a)), ～Q(a, f(a, a)), ～Q(f(a, a), a), ～Q(f(a, a), f(a, a)), …｝ 指定 a對(duì)應(yīng)2得H解釋?zhuān)? I2*＝｛～P(a), Q(a, a), P(f(a, a)), ～Q(a, f(a, a)), Q(f(a, a), a), ～Q(f(a, a), f(a, a)), …｝,.,6/27/2018,12,對(duì)應(yīng)于I的H解釋I*,定義（對(duì)應(yīng)于I的H解釋I*） 設(shè)I是子句集S在區(qū)域D上的解釋。H是S的H域。 ? 是如下遞歸定義的H到D的映射： 1） ①若S中有常量符號(hào),H0是出現(xiàn)在S中所有常量符號(hào)的集合。 對(duì)任意a?H0，規(guī)定? (a)=I(a)． ②若S中無(wú)常量符號(hào),H0={a}。 規(guī)定? (a)=d,d∈D。 2）對(duì)任意(h1,…,hn)?Hin,及S中任意n元函數(shù)符號(hào)f(x1,…,xn) , 規(guī)定?(f(h1，…，hn)) =I(f(h1?，…，hn?)) 。,.,6/27/2018,13,對(duì)應(yīng)于I的H解釋I*,對(duì)應(yīng)于I的H解釋I*是如下的一個(gè)H解釋?zhuān)? 任取S中n元謂詞符號(hào)P(x1,…,xn)， 任取(h1,…,hn)?Hn，規(guī)定 TI*(P(h1，…，hn))=TI(P(h1?，…，hn?)),.,6/27/2018,14,引理 如果某區(qū)域D上的解釋I滿足子句集S， 則對(duì)應(yīng)于I的任意一個(gè)H解釋I*也滿足S。 證明：令S= ?x1 … ?xn (C1? … ?Cm)，其中Ci為子句（i=1, … ,m）。由已知TI(S)=T，即對(duì)任意（x1，…，xn）?Dn，都有TI(Ci（x1，…，xn）)=T, i=1, … ,m,,.,6/27/2018,15,,因?yàn)閷?duì)S中任意r元謂詞符號(hào)P（x1，…，xr）和任意（h1，…，hr）?Hr，都有 TI*( P（h1，…，hr）)=TI(P（h1?，…，hr?）) 其中（h1?，…，hr?）?Dr。 所以，對(duì)任意（h1，…，hn）?Hn，都有 TI*( Ci（h1，…，hn）)=TI(Ci（h1?，…，hn?）) 其中（h1?，…，hn?）?Dn。 i=1, … ,m。 故對(duì)任意（h1，…，hn）?Hn ，都有 TI*(Ci（h1，…，hn）)=T, 故TI*(S)=T，即I*滿足S。,.,6/27/2018,16,,只考慮子句集的H解釋是否夠用？ 定理 子句集S恒假當(dāng)且僅當(dāng)S被其所有H解釋弄假。 證明: 必要性顯然。 充分性。假設(shè)S被其所有H解釋弄假，而S又是可滿足的。 設(shè)解釋I滿足S，于是由引理知，對(duì)應(yīng)于I的H解釋I*也滿足 S，矛盾．故S是不可滿足的． 從現(xiàn)在起，如不特別指出，提到的解釋都是指H解釋?zhuān)?.,6/27/2018,17,結(jié)論,l）子句 C的基例 C’被解釋 I滿足，當(dāng)且僅當(dāng) C’中的一個(gè)基文字L’出現(xiàn)在 I中． C= P(x) ? ～Q(f(y),a) ? R(z) C’= P(a) ? ～Q(f(a),a) ? R(f(a)),.,6/27/2018,18,,2）子句C被解釋I滿足，當(dāng)且僅當(dāng) C的每一個(gè)基例都被I滿足． 3）子句 C被解釋 I弄假，當(dāng)且僅當(dāng) 至少有一個(gè)C的基例C’被I弄假。,.,6/27/2018,19,例.,C=～P(x)?Q(f(x)) I1={～P(a),～Q(a),～P(f(a)),～Q(f(a)),～P(f(f(a))),～Q(f(f(a))),…} I2={P(a),Q(a),P(f(a)),Q(f(a)),P(f(f(a))),Q(f(f(a))),…} I3={P(a),～Q(a),P(f(a)),～Q(f(a)),P(f(f(a))),～Q(f(f(a))),…} 顯然，I1，I2滿足C，I3弄假C。,.,6/27/2018,20,,4）子句集S不可滿足，當(dāng)且僅當(dāng) 對(duì)每個(gè)解釋I，至少有一個(gè)S中某個(gè)子句C的基例C’被I弄假。,.,6/27/2018,21,6.2 Herbrand定理,Herbrand定理是符號(hào)邏輯中一個(gè)很重要的定理．Herbrand定理就是使用語(yǔ)義樹(shù)的方法，把需要考慮無(wú)窮個(gè)H解釋的問(wèn)題，變成只考慮有限個(gè)解釋的問(wèn)題．,.,6/27/2018,22,一、語(yǔ)義樹(shù),定義(互補(bǔ)對(duì)) 設(shè) A是原子，兩個(gè)文字A和～A都是另一個(gè)的補(bǔ)，集合｛A，～A｝稱(chēng)為一個(gè)互補(bǔ)對(duì)． 定義(Tautology,重言式) 含有互補(bǔ)對(duì)的子句．,.,6/27/2018,23,定義 （語(yǔ)義樹(shù)） 設(shè)S是子句集，A是S的原子集．關(guān)于S的語(yǔ)義樹(shù)是一棵向下生長(zhǎng)的樹(shù)T．在樹(shù)的每一節(jié)上都以如下方式附著A中有限個(gè)原子或原子的否定： 1）對(duì)于樹(shù)中每一個(gè)節(jié)點(diǎn)N，只能向下引出有限的直接的節(jié) L1，…，Ln． 設(shè)Qi是附著在Li上所有文字的合取，i=1, … ,n， 則Q1?…?Qn是一個(gè)恒真的命題公式． 2）對(duì)樹(shù)中每一個(gè)節(jié)點(diǎn) N，設(shè) I（N）是樹(shù)T由根向下到節(jié)點(diǎn) N 的所有節(jié)上附著文字的并集， 則I（N）不含任何互補(bǔ)對(duì)．,語(yǔ)義樹(shù),.,6/27/2018,24,完全語(yǔ)義樹(shù),定義（完全語(yǔ)義樹(shù)） 設(shè)A={A1,…,An,…｝是子句集S的原子集． S的一個(gè)語(yǔ)義樹(shù)是完全的，當(dāng)且僅當(dāng) 對(duì)于語(yǔ)義樹(shù)中每一個(gè)尖端節(jié)點(diǎn)N（即從N不再 生出節(jié)的那種節(jié)點(diǎn)），都有 Ai或～Ai有且僅有一個(gè)屬于I(N),i=1,…,k,…,.,6/27/2018,25,,例. 設(shè)A=｛P，Q，R｝是子句集S的原子集， 完全語(yǔ)義樹(shù)(正規(guī)完全語(yǔ)義樹(shù) ),.,6/27/2018,26,,,.,6/27/2018,27,例. 設(shè) S={P(x), Q(f(x))}S的原子集為A={P(a), Q(a), P(f(a)), Q(f(a)), P(f(f(a))), Q(f(f(a))), …},,.,6/27/2018,28,語(yǔ)義樹(shù)與解釋,S的完全語(yǔ)義樹(shù)的每一個(gè)分枝都對(duì)應(yīng)著S的一個(gè)解釋?zhuān)?定義（部分解釋?zhuān)?duì)于子句集S的語(yǔ)義樹(shù)中的每一個(gè)節(jié)點(diǎn)N,I(N)是S的某個(gè)解釋的子集，稱(chēng)I(N)為S的部分解釋。 S的任意解釋都對(duì)應(yīng)著S的完全語(yǔ)義樹(shù)中的一條分枝？ 綜合： 子句集S的一棵完全語(yǔ)義樹(shù)對(duì)應(yīng)著S的所有解釋。,.,6/27/2018,29,證明: 若不然，設(shè)T中節(jié)點(diǎn)N向下生出的n個(gè)節(jié)L1，…，Ln的每個(gè)節(jié)Li上，都至少有一個(gè)文字Ai不在I中． 由語(yǔ)義樹(shù)的定義知：Q1?…?Qn是恒真公式,其中Qi表示Li 上所有文字的合取，i=1, …, n。將Q1?…?Qn化為合取范式： Q1?…?Qn＝（A1?A2?…?An）?(…)? …? (…) 因?yàn)槊恳粋€(gè)析取式中都必須有一個(gè)互補(bǔ)對(duì)。不妨設(shè) A1＝～A2,于是A2,～A2都不在I中,這與I是一個(gè)解釋矛盾。 結(jié)論：對(duì)S的任意解釋I，都可以從S的完全語(yǔ)義樹(shù)的根點(diǎn)出發(fā)，向下找出一條分枝，使該分枝對(duì)應(yīng)著解釋I。,引理 設(shè)T是子句集S的完全語(yǔ)義樹(shù)，I是S的一個(gè)解釋。于是T中任意節(jié)點(diǎn)向下生出的直接節(jié)中，必有一節(jié)，其上所有文字都在I中。,.,6/27/2018,30,子句集的封閉語(yǔ)義樹(shù),定義（失效點(diǎn)） 稱(chēng)語(yǔ)義樹(shù)T中的節(jié)點(diǎn)N為失效點(diǎn)，如果 (1)I(N)弄假S中某個(gè)子句的某個(gè)基例； (2)I(N’)不弄假S中任意子句的任意基例，其中N’是 N的任意祖先節(jié)點(diǎn)。 定義（封閉語(yǔ)義樹(shù)） 語(yǔ)義樹(shù)T是封閉的，當(dāng)且僅當(dāng)T的每—個(gè)分枝的終點(diǎn)都是失效點(diǎn)。 定義（推理點(diǎn)）稱(chēng)封閉語(yǔ)義樹(shù)的節(jié)點(diǎn) N為推理點(diǎn)，如果N的所有直接下降節(jié)點(diǎn)都是失效點(diǎn)．,.,6/27/2018,31,例. 設(shè)S={P, ～P?R, ～P?～Q, ～P?～R}。,S的原子集 A={P, Q, R},,,,,,,,,,,,,,,,P,~P,Q,~Q,Q,~Q,R,~R,R,~R,R,~R,R,~R,.,6/27/2018,32,練習(xí),設(shè)子句集 S={～P(x)∨Q(x),P(f(x)), ～Q(f(x))} 分別畫(huà)出S的完全語(yǔ)義樹(shù)與 封閉語(yǔ)義樹(shù)。,.,6/27/2018,33,二、Herbrand定理,Herbrand定理I．子句集S是不可滿足的，當(dāng)且僅當(dāng)對(duì)應(yīng)于S的每一個(gè)完全語(yǔ)義樹(shù)都存在一個(gè)有限的封閉語(yǔ)義樹(shù)． 證明: 必要性： 若S是不可滿足的，設(shè)T是S的完全語(yǔ)義樹(shù)． 對(duì)T的每一個(gè)分枝B,令I(lǐng)B是附著在B上所有文字的集合， 則IB是S的一個(gè)解釋,故IB弄假S中某子句C的某個(gè)基例C’． 由于C’是有限的，所以B上存在一個(gè)節(jié)點(diǎn)NB使得部分解 釋I（NB）弄假C’，于是分枝B上存在失效點(diǎn)． 因此，對(duì)T中每一分枝都存在一個(gè)失效點(diǎn)，于是從T得到 S的一個(gè)封閉語(yǔ)義樹(shù)T’。,.,6/27/2018,34,Herbrand定理I．子句集S是不可滿足的，當(dāng)且僅當(dāng)對(duì)應(yīng)于S的每一個(gè)完全語(yǔ)義樹(shù)都存在一個(gè)有限的封閉語(yǔ)義樹(shù)．,(有限性) 因?yàn)榉忾]語(yǔ)義樹(shù)T’中每一個(gè)節(jié)點(diǎn)只能向下生長(zhǎng)有限個(gè)節(jié),故T’必有有限個(gè)節(jié)點(diǎn).否則,由Konig無(wú)限性引理,T’中必有一條無(wú)窮的分枝,此無(wú)窮分枝上當(dāng)然沒(méi)有失效點(diǎn),矛盾。 （Konig無(wú)限性引理：在一個(gè)其點(diǎn)之次數(shù)有限的無(wú)限有向樹(shù)中，必有一源于根的無(wú)限路。 ） 充分性： 若S的每一個(gè)完全語(yǔ)義樹(shù)T都對(duì)應(yīng)著一個(gè)有限封閉語(yǔ)義樹(shù) T’，則T的每條分枝上都有一個(gè)失效點(diǎn)。因?yàn)镾的任一解 釋都對(duì)應(yīng)T的某一條分枝，所以每一個(gè)解釋都弄假S， 故S是不可滿足的。,.,6/27/2018,35,Herbrand定理II 子句集S是不可滿足的，當(dāng)且僅當(dāng)存在S的一個(gè)有限不可滿足的S的基例集S’。,證明: 必要性： 若S恒假，設(shè)T是S的完全語(yǔ)義樹(shù)，由 Herbrand定理I知，有一個(gè)有限封閉 語(yǔ)義樹(shù) T’對(duì)應(yīng)著T。 令S’是被 T’中所有失效點(diǎn)弄假的所有 基例（S中某些子句的基例）的集合。 因?yàn)門(mén)’中失效點(diǎn)的個(gè)數(shù)有限，所以S’ 是有限集合。 任取S’的一解釋I’，則I’是S的某個(gè)解 釋I的子集，而解釋I是T中一個(gè)分 枝，所以，I弄假S’中子句C’，故 I弄假S’。因?yàn)镮’?I,且I’是S’的解釋,故 I’弄假S’．由I’的任意性知S’不可滿足。,S={P(x), ～P(a)∨～P(b), Q(f(x))} H={a,b,f(a),f(b),f(f(a)),f(f(b)),…} A={P(a),P(b),Q(a),Q(b),…} S’={P(a), P(b), ～P(a)∨～P(b)},.,6/27/2018,36,Herbrand定理II 子句集S是不可滿足的，當(dāng)且僅當(dāng)存在S的一個(gè)有限不可滿足的S的基例集S’。,充分性：假設(shè)S有一個(gè)有限的不可滿足的基例集S’。 任取S的解釋I， 因?yàn)镾的每一個(gè)解釋I都包含著S’的一個(gè)解釋I’，而S’是不可滿足的，所以S的任一解釋I都弄假S’，故I弄假S’中至少一個(gè)子句，即I弄假S中至少一個(gè)子句的基例，亦即I弄假S。 由I的任意性，知S是不可滿足的。,.,6/27/2018,37,,Herbrand定理II提出了一種證明子句集S的不可滿足性的方法：如果存在這樣一個(gè)機(jī)械程序，它可以逐次生成S中子句的基例集 S0’，…，Sn’，并逐次地檢查S0’，…，Sn’，…的不可滿足性，那么根據(jù) Herbrand定理，如果 S是不可滿足的，則這個(gè)程序一定可以找到一個(gè)有限數(shù)N，使SN’是不可滿足的。,.,6/27/2018,38,使用Herbrand定理的機(jī)器證明過(guò)程,Gilmore過(guò)程 D-P過(guò)程,.,6/27/2018,39,Gilmore過(guò)程（1960年）,逐次地生成S0’， S1’…，Sn’，…，其中Si’是用S的i級(jí)常量集合Hi中的常量，代替S中子句的變量，而得到的S的所有基例之集合。 對(duì)于每一個(gè)Si’，可以使用命題邏輯中的任意的方法去檢查Si’的不可滿足性。 Gilmore使用了所謂乘法方法：即將Si’化為析取范式。如果其中任意一個(gè)合取項(xiàng)包含一個(gè)互補(bǔ)對(duì)，則可以刪除這個(gè)合取項(xiàng)，最后，如果某個(gè)Si’是空的，則Si’是不可滿足的。 當(dāng)S不可滿足時(shí)，該算法一定結(jié)束(半可判定)。,.,6/27/2018,40,,例. S={P(a), ～P(x) ?Q(f(x)), ～Q(f(a)) } H0={a} S0=P(a) ?(～P(a) ?Q(f(a))) ?～Q(f(a)) =(P(a)?～P(a)?～Q(f(a)))?(P(a) ?Q(f(a)))?～Q(f(a))) =??? =? 所以，S是不可滿足的。 該算法具有指數(shù)復(fù)雜性，為此提出了改進(jìn)規(guī)則，稱(chēng)為Davis-Putnam預(yù)處理----檢驗(yàn)基子句集不可滿足性。,.,6/27/2018,41,D-P過(guò)程,設(shè)S是基子句集 Tautology刪除規(guī)則 設(shè)S’為刪去S中所有的Tautology所剩子句集， 則 S恒假 iff S’恒假。,.,6/27/2018,42,,單文字規(guī)則 若S中有一個(gè)單元基子句L， 令S’為刪除S中包含L的所有基子句所剩子句集， 則： (1) 若S’為空集，則S可滿足。 (2) 否則， 令S’’為刪除S’中所有文字～L所得子句集 （若S’ 中有單元基子句～L，則刪文字～L 得空子句）， 于是， S恒假 iff S’’恒假。 S=L∧(L∨C1’) ∧… ∧(L∨Ci’) ∧ (～L∨Ci+1’) ∧… ∧ (～L∨Cj’) ∧ Cj+1 ∧… ∧ Cn,.,6/27/2018,43,,定義（純文字）：稱(chēng)S的基子句中文字L是純的，如果～L不出現(xiàn)在S中。 純文字規(guī)則 設(shè)L是S中純文字，且S’為刪除S中所有包含L的基子句所 剩子句集，則 (1)若S’為空集，則S可滿足。 (2) 否則，S恒假 iff S’恒假。 S=(L∨C1’) ∧… ∧(L∨Ci’) ∧ Ci+1 ∧… ∧ Cn,.,6/27/2018,44,,分裂規(guī)則 若S=(A1 ?L) ?… ? (Am ?L) ? (B1 ? ～L) ? … ? (Bn ? ～L) ?R 其中A i , Bi ,R都不含L或～L，令 S1 =A1 ?… ? Am ?R S2= B1 ? … ? Bn ?R 則S恒假 iff S1 ， S2同時(shí)恒假。,.,6/27/2018,45,Davis-Putnam方法練習(xí),S= (P?Q?～R) ?(P?～Q) ?～P ?R ?U S= (P?～Q) ?(～P?Q) ? (Q?～R) ? (～Q?～R) S= (P?Q) ?(P?～Q) ? (R?Q) ? (R?～Q),.,6/27/2018,46,Herbrand定理的主要障礙,要求生成關(guān)于子句集S的基例集 S1’, S2’, …。在多數(shù)情況下，這些集合的元數(shù)是以指數(shù)方式增加的： 例.S={P(x,g(x),y,h(x,y),z,k(x,y,z)),～P(u,v,e(v),w,f(v,w),x)} H0={a} H1={a, g(a), h(a, a), k(a, a, a), e(a), f(a, a)} … S0’={P(a,g(a),a,h(a,a),a,k(a,a,a)),～P(a,a,e(a),a,f(a,a),a)} S1’={(6?6?6)+(6?6?6?6)=216+1296=1512個(gè)元素} S5’是不可滿足的，但是H5’是1065數(shù)量級(jí)個(gè)元素，而S5’有10260數(shù)量級(jí)的元素。想將S5’存儲(chǔ)起來(lái)都是不可能的，更不要說(shuō)是檢查它的不可滿足性了。,.,6/27/2018,47,為了避免像Herbrand定理所要求的那樣去生成子句的基例集，J.A.Robinson于1965年提出了歸結(jié)原理，歸結(jié)原理可以直接應(yīng)用到任意子句集S上（不一定是基子句集），去檢查S的不可滿足性。 歸結(jié)原理的本質(zhì)思想是去檢查子句集S是否包含一個(gè)空子句?: 如果S包含?，則S是不可滿足的。 如果S不包含?，則去檢查?是否可由S推導(dǎo)出來(lái)。 當(dāng)然這個(gè)推理規(guī)則必須保證推出的子句是原親本子句的邏輯結(jié)果。歸結(jié)原理就是具有這種性質(zhì)的一種推理規(guī)則。,歸結(jié)原理思想,.,6/27/2018,48,命題邏輯中的歸結(jié)原理,,.,6/27/2018,49,歸結(jié)式,定義（歸結(jié)式） 對(duì)任意兩個(gè)基子句C1和C2。如果C1中存在文字L1，C2中存在文字L2，且L1＝～L2， 則從C1和C2中分別刪除L1和L2，將C1和C2的剩余部分析取起來(lái)構(gòu)成的子句，稱(chēng)為C1和C2的歸結(jié)式，記為R(C1, C2)。 C1和C2稱(chēng)為親本子句。,.,6/27/2018,50,練習(xí):求下述各子句對(duì)的歸結(jié)式,C1= ～P?Q?R, C2=～Q?S C1= P?Q?～R, C2=～P? R?Q,.,6/27/2018,51,定理 設(shè)C1和C2是兩個(gè)基子句， R(C1, C2) 是C1，C2的歸結(jié)式，則R(C1, C2)是C1和C2的邏輯結(jié)果。 證明： 設(shè) C1=L ?C1’, C2=～L?C2’。于是 R(C1, C2) ＝C1’ ?C2’ 設(shè)I是C1和C2的一個(gè)解釋?zhuān)覞M足C1也滿足C2。因?yàn)長(zhǎng)和～L中有一個(gè)在I下為假，不妨設(shè)為L(zhǎng)。于是C1’非空，且在I下為真。故R(C1, C2)在I下為真。,命題邏輯歸結(jié)方法的可靠性,.,6/27/2018,52,歸結(jié)演繹,定義（歸結(jié)演繹） 設(shè)S是子句集。從S推出子句C的一個(gè)歸結(jié)演繹是如下一個(gè)有限子句序列： C1，C2，…，Ck 其中Ci或者是S中子句，或者是Cj和Cr的歸結(jié)式 (j?i, r? i)； 并且Ck＝C。 稱(chēng)從子句集S演繹出子句C，是指存在一個(gè)從S推出C的演繹。 定理 若從子句集S可以演繹出子句C，則C是S的邏輯結(jié)果。 推論 若子句集S是可滿足的， 則S推出的任意子句也是可滿足的。,.,6/27/2018,53,,定義 從S推出空子句的演繹稱(chēng)為一個(gè)反駁（反證） ，或稱(chēng)為S的一個(gè)證明。 結(jié)論：若從基子句集S可演繹出空子句，則S是不可滿足的。 演繹樹(shù)：從子句集S出發(fā)，通過(guò)歸結(jié)原理可得到一個(gè)向下的演繹樹(shù)，其每個(gè)初始節(jié)點(diǎn)上附著一個(gè)S中子句，每個(gè)非初始節(jié)點(diǎn)上附著一個(gè)其前任節(jié)點(diǎn)上子句的歸結(jié)式。,.,6/27/2018,54,例. S={P?Q, ～P?Q, P?～Q, ～P?～Q },歸結(jié)演繹： (1) P?Q (2) ～P?Q (3) P?～Q (4) ～P?～Q (5) Q 由(1)、(2) (6) ～Q 由(3)、(4) (7) ? 由(5)、(6),.,6/27/2018,55,歸結(jié)原理一般過(guò)程:,1)建立子句集S。 2)如果S含空子句，則結(jié)束。 3)從子句集S出發(fā),僅對(duì)S的子句間使用歸結(jié)推理規(guī)則。 4)如果得出空子句，則結(jié)束。 5)將所得歸結(jié)式仍放入S中。 6)對(duì)新的子句集使用歸結(jié)推理規(guī)則。轉(zhuǎn)4)。,.,6/27/2018,56,例.證明(P ?Q) ?~Q ? ~p,首先建立子句集: S={~P?Q, ~Q , P} 歸結(jié)演繹: (1) ~P? Q (2) ~ Q (3) P (4) ~P (1)(2)歸結(jié) (5) ? (3)(4)歸結(jié),.,6/27/2018,57,命題邏輯歸結(jié)原理的完備性,定理 如果基子句集S是不可滿足的， 則存在從S推出空子句的歸結(jié)演繹。 證明： 設(shè)M是S的原子集，對(duì)M的元素?cái)?shù)|M|用歸納法。 當(dāng)|M|=1時(shí)，設(shè)原子為P。 若?∈S ，得證。 否則，因?yàn)镾是不可滿足的，于是，S中必包含單元子 句P和～P，而P和～P的歸結(jié)式是?，所以存在從S推出?的 歸結(jié)演繹。 假設(shè)|M|?n (n≥2) 時(shí)，定理成立。往證 |M|＝n時(shí)定理成立。,.,6/27/2018,58,,取M中任意一原子P，做如下兩個(gè)子句集： S’：將S中所有含P的子句刪除，然后在剩下的子 句中刪除文字～P； S”：將S中所有含～P的子句刪除，然后在剩下的 子句中刪除文字P。 顯然，S’和S”都不可滿足，且它們的原子集的元 素?cái)?shù)都小于n。根據(jù)歸納假設(shè)，存在從S’推出 ? 的 歸結(jié)演繹D1，從S”推出?的歸結(jié)演繹D2。,.,6/27/2018,59,,S={P∨C1’, … ,P∨Ci’ , ～P∨Ci+1’,… ,～P∨Cj’, Cj+1 ,… , Cn} S’={Ci+1’,… ,Cj’,Cj+1 ,… , Cn} S’’={C1’, … ,Ci’ , Cj+1 ,… , Cn} 例： S={P?Q, P?～Q, ～P?R, ～ R} M={P,Q,R},.,6/27/2018,60,,在D1中，將S’中所有不是S中的子句，通過(guò) 添加文字～P而恢復(fù)成S中子句，于是，得到從S 推出 ? 或者～P的歸結(jié)演繹D1’。 用同樣方法從D2可得一個(gè)從S推出 ? 或者P的 歸結(jié)演繹D2’。 顯然，從D1’和D2’就不難得到一個(gè)從S推出 ? 的 歸結(jié)演繹D。 歸納法完成。,.,6/27/2018,61,,Resolution Principle 兩種譯法： 歸結(jié)原理：從內(nèi)部看 劉敘華，一種新的語(yǔ)義歸結(jié)原理，吉林大學(xué)學(xué)報(bào)，1978。 消解原理：從外部看 馬希文，機(jī)器證明及其應(yīng)用，計(jì)算機(jī)應(yīng)用， 1978。,.,6/27/2018,62,6.3 合一算法,,.,6/27/2018,63,,例1 C1：P(x) ? Q(y) C2：~P(a) ? R(z) 例2 C1：P(x) ? Q(x) C2：~P(f(x)) ? R(x) 替換和合一是為了處理謂詞邏輯中子句之間的模式匹配而引進(jìn).,.,6/27/2018,64,一、替換與最一般合一替換,定義(替換)一個(gè)替換是形如{t1/v1, … , tn/vn }的一個(gè)有限集合，其中vi是變量符號(hào)，ti是不同于vi的項(xiàng)。并且在此集合中沒(méi)有在斜線符號(hào)后面有相同變量符號(hào)的兩個(gè)元素，稱(chēng)ti為替換的分子，vi為替換的分母。 例. {a/x, g(y)/y, f(g(b))/z}是替換; {x/x}, {y/f(x)}, {a/x, g(y)/y, f(g(b))/y}不是替換; 基替換:當(dāng)t1,…,tn是基項(xiàng)時(shí)，稱(chēng)此替換為基替換。 空替換：沒(méi)有元素的替換稱(chēng)為空替換，記為?。,.,6/27/2018,65,替換,定義（改名） 設(shè)替換 ? ={ t1/x1, … , tn/xn } 如果t1, … , tn是不同的變量符號(hào)，則稱(chēng)?為一個(gè)改 名替換，簡(jiǎn)稱(chēng)改名。 替換作用對(duì)象：表達(dá)式（項(xiàng)、項(xiàng)集、原子、原子集、 文字、子句、子句集） 基表達(dá)式：沒(méi)有變量符號(hào)的表達(dá)式。 子表達(dá)式：出現(xiàn)在表達(dá)式E中的表達(dá)式稱(chēng)為E的子 表達(dá)式。,.,6/27/2018,66,E的例,定義（E的例） 設(shè) ? ={ t1/v1, … , tn/vn }是一個(gè)替換，E是一個(gè)表達(dá)式。將E中出現(xiàn)的每一個(gè)變量符號(hào)，vi (1? i ?n) ，都用項(xiàng)ti替換，這樣得到的表達(dá)式記為E?。稱(chēng)E? 為E的例。 若E? 不含變量，則E? 為E的基例。 例. 令 ? = {a/x, f(b)/y, c/z}，E=P(x, y, z) 于是E的例（也是E的基例）為 E? = P(a, f(b), c),,.,6/27/2018,67,,練習(xí)： E=P(x, g(y), h(x,z)), ?={a/x, f(b)/y, g(w)/z} E?=P(a, g(f(b)), h(a,g(w))) E=P(x, y, z), ?={y/x, z/y} E?=P(y, z, z). E??P(z, z, z).,.,6/27/2018,68,替換的乘積,定義（替換的乘積）設(shè)? ={ t1/x1, … , tn/xn }，? ={ u1/y1, … , um/ym} 是兩個(gè)替換。將下面集合 { t1?/x1, … , tn?/xn , u1/y1, … , um/ym } 中任意符合下面條件的元素刪除： 1）ui/yi，當(dāng)yi?{x1, … , xn }時(shí)； 2）ti?/xi，當(dāng)ti? = xi 時(shí)。 如此得到一個(gè)替換，稱(chēng)為?與?的乘積，記為? ??。 例. 令 ? ={f(y)/x, z/y} ? ={a/x, b/y, y/z} 于是得集合 { t1?/x1, t2?/x2 , u1/y1, u2/y2 , u3/y3 } = {f(b)/x, y/y, a/x, b/y, y/z } ? 與?的乘積為 ? ?? = {f(b)/x, y/z },.,6/27/2018,69,,?={a/x}, ?={b/x} ???={a/x} ???={b/x} 可見(jiàn)：??? ? ???,.,6/27/2018,70,,例子: E=P(x, y, z) ?={a/x, f(z)/y, w/z} E?=P(a, f(z), w) ?={t/z, g(b)/w} (E?)?=P(a, f(t), g(b)) ???={a/x, f(t)/y, g(b)/z,g(b)/w} E???=P(a, f(t), g(b)),.,6/27/2018,71,引理 若E是表達(dá)式，?，?是兩個(gè)替換， 則E (? ??) = (E?)?,證明： 設(shè)vi是E中任意一個(gè)變量符號(hào)，而 ? ={ t1/x1, … , tn/xn }， ? ={ u1/y1, … , um/ym } 若vi既不在{ x1, … , xn }中，也不在{ y1, … , ym }中，則vi在E (? ??)中和在(E?)?中都不變。 若vi=xj (1?j?n)，則E中的vi，在(E?)?中先變成tj，然后再變成tj?；E中的vi在E(???)中立即就變成了tj?。故E中vi在(E?)?中和在E(???)中有相同變化。 若vi=yj (1?j?m)，且yj?{ x1,…,xn }，則E中vi在(E?)?中變?yōu)閡j;E中vi在E(???)中也變?yōu)閡j(注意:yj?{x1,…, xn}，所以u(píng)j/yj????），故E中vi在(E?)?中和在E (???)中有相同變化。 由于vi的任意性，故引理得證。,.,6/27/2018,72,引理 設(shè)?，?，? 是三個(gè)替換， 于是(???)??＝??(???),證明： 設(shè)E是任一表達(dá)式，由上面引理知 E((???)??) =(E(???))? = ((E?)?)? E(??(???)) =(E?) (??) = ((E?)?)? 所以 E((???)??) = E(??(???)) 由于E的任意性，故 (???)??＝??(???),.,6/27/2018,73,,定義(合一)稱(chēng)替換?是表達(dá)式集合{E1,…,Ek}的 合一，當(dāng)且僅當(dāng)E1?＝E2?=…=Ek?。 表達(dá)式集合｛E1, … , Ek｝稱(chēng)為可合一的，如果存在關(guān)于此集合的一個(gè)合一。 定義(最一般合一) 表達(dá)式集合｛E1, … , Ek｝的合一? 稱(chēng)為是最一般合一(most general unifier, 簡(jiǎn)寫(xiě)為mgu)，當(dāng)且僅當(dāng)對(duì)此集合的每一個(gè)合一?，都存在替換?，使得 ?＝???,.,6/27/2018,74,,例. 表達(dá)式集合｛P(a, y), P(x, f(b))｝是可合一的，其最一般合一?＝{a/x, f(b)/y}。顯然，這也是此集合的mgu。 ？ 表達(dá)式集合｛P(a, b), P(x, f(b))｝是否可合一？ 例. 表達(dá)式集合｛P(x), P(f(y))｝是可合一的，其最一般合一?＝{f(y)/x} ?＝{f(a)/x, a/y}也是合一，有替換 ?={a/y}，使 ?＝???={f(y)/x}?{a/y},.,6/27/2018,75,,例 S={P(x) ? ~Q(x),~P(y), Q(b)} {P(x),P(y)}可合一，?＝{a/x, a/y}是合一， 其mgu ?＝{x/y}，有替換 ?={a/x}，使 ?＝???= {x/y} ?{a/x},.,6/27/2018,76,二、合一算法,定義（差異集合） 設(shè)W是非空表達(dá)式集合，W的差異集合是如下一個(gè)集合：首先找出W的所有表達(dá)式中不是都相同的第一個(gè)符號(hào)，然后從W的每一個(gè)表達(dá)式中抽出占有這個(gè)符號(hào)位置的子表達(dá)式。所有這些子表達(dá)式組成的集合稱(chēng)為這步找到的W的差異集合D。,.,6/27/2018,77,W不可合一的三種情況,（1）若D中無(wú)變量符號(hào)為元素，則W是不可合一的。 例. W={P(f(x)), P(g(x))} D={f(x), g(x)} （2）若D中有奇異元素和非奇異元素，則W是不可合一的。 例. W={P(x), P(x, y)} D={⊙, y} （3）若D中元素有變量符號(hào)x和項(xiàng)t，且x出現(xiàn)在t中，則W是不可合一的。 例. W={P(x), P(f(x))} D={x, f(x)},.,6/27/2018,78,,換名: {P(f(x), x), P(x, a)}; 如果不換名：D={f(x), x}. 換名: {P(f(y), y), P(x, a)}; mgu: {f(a)/x, a/y},.,6/27/2018,79,步驟1：置 k=0, Wk=W, ?k=? 步驟2：若Wk只有一個(gè)元素，則停止，?k是W的最一般合一； 否則，找出Wk的差異集合Dk。 步驟3：若Dk非奇異，Dk中存在元素vk和tk，其中vk是變量符號(hào)，并且 不出現(xiàn)在tk中，則轉(zhuǎn)步驟4； 否則，算法停止，W是不可合一的。 步驟4：令 ?k+1=?k?{tk/vk}，Wk+1=Wk （注：Wk+1=W ） 步驟5：置 k=k+1，轉(zhuǎn)步驟2。,合一算法（Unification algorithm）,,,.,6/27/2018,80,例. 令 W={Q(f(a), g(x)), Q(y, y)}, 求W的mgu。,步驟1： k=0, W0=W, ?0=?。 步驟2： D0 ={f(a), y}。 步驟3：有v0=?y ?D0，v0不出現(xiàn)在t0＝f(a)中。 步驟4：令 ?1=?0?{t0/v0}={f(a)/y}, W1={Q(f(a), g(x)), Q(f(a), f(a))} 步驟5：k=k+1=1 步驟2： D1 ={g(x), f(a) }。 步驟3：D1中無(wú)變量符號(hào)，算法停止，W不可合一。 ？ 若令W={Q(f(a), g(x)), Q(y, z)}, W是否可合一？,.,6/27/2018,81,例 令 W= {P(a, x, f(g(y))), P(z, f(z), f(u))}， 求出W的mgu。,,步驟1：k=0,W0=W, ?0=? 。 步驟2： D0 ={a, z}。 步驟3：有v0=?z ?D0，v0不出現(xiàn)在t0＝a中。 步驟4：令 ?1=?0?{t0/v0}=??{a/z}={a/z}， W1=W0{t0/v0}={P(a,x,f(g(y))),P(z,f(z),f(u))}{a/z}={P(a,x,f(g(y))),P(a,f(a),f(u))} 步驟5：k=k+1=1 步驟2： D1 ={x, f(a) }。 步驟3：有v1=?x ?D1，且v1不出現(xiàn)在t1＝f(a)中。 步驟4：令 ?2=?1?{t1/v1}={a/z}? { f(a)/x }={a/z, f(a)/x }， W2=W1{t1/v1}={P(a,x,f(g(y))),P(a,f(a),f(u))}{f(a)/x} ={P(a,f(a),f(g(y))),P(a,f(a),f(u))},.,6/27/2018,82,例.,步驟5：k=k+1=2 步驟2： D2 ={g(y), u}。 步驟3：有v2=?u ?D2，且v2不出現(xiàn)在t2＝g(y)中。 步驟4：令 ?3=?2?{t2/v2}={a/z, f(a)/x }? { g(y)/u } ={a/z, f(a)/x, g(y)/u }， W3=W2{t2/v2}={P(a, f(a), f(g(y))), P(a, f(a), f(u))}{ g(y)/u } ={P(a, f(a), f(g(y)))} 步驟5:k=k+1=3 步驟2：W3只有一個(gè)元素。算法停止。 ?3={a/z, f(a)/x, g(y)/u } 是W的最一般合一。,.,6/27/2018,83,定理 若W是關(guān)于表達(dá)式的有限非空可合一集合，則合一算法終將結(jié)束在步驟2，并且最后的?k是W的最一般合一。,證明： （1）終止性。 否則將產(chǎn)生一個(gè)無(wú)窮序列： W ， W ，…， W ，… 其中每一個(gè)直接后繼集合比它的前任都少一個(gè)變量符號(hào)（注意：W 包含vk，而W 不包含vk）。但這是不可能的，因?yàn)閃僅含有限個(gè)變量符號(hào)。 （2） ?k是W的合一。若算法停止在步驟2，則Wk=W只含有一個(gè)元素，所以?k是W的合一。,,,,,,.,6/27/2018,84,,（3）用歸納法證明算法必不會(huì)停止在步驟3，并且對(duì)任意W的一個(gè)合一?，任意k，都存在替換?k，使得 ?=?k??k 亦即?k是W的mgu。 當(dāng)k=0時(shí)，因?0=?，取?0=?，于是?=???=?0??0。,.,6/27/2018,85,假設(shè)對(duì)0?k?n，?=?k??k成立。 往證：存在?n+1，使得?=?n+1??n+1。 若W 只含有一個(gè)元素，則合一算法結(jié)束在步驟2。因?yàn)?=?n??n，且?n是W的合一，故?n是W的mgu。定理得證。 若W 不只含有一個(gè)元素,按照算法,將找出W的差異集合Dn。 因?yàn)?=?n??n是W的合一，所以W中表達(dá)式經(jīng)替換?作用后都變成同一個(gè)相同的表達(dá)式。而W中表達(dá)式經(jīng)?n作用后，產(chǎn)生了差異集合Dn，所以Dn必須被?n所統(tǒng)一，即?n是D n的合一。,.,6/27/2018,86,,因?yàn)镈n是可合一的（?n就是Dn的合一），所以必有變量符號(hào)vn?Dn；Dn中至少有兩個(gè)不同元素。所以可設(shè)tn?Dn，且tn≠vn。顯然，變量符號(hào)vn不出現(xiàn)在tn中（否則，vn?n≠ tn?n，這與?n是Dn的合一矛盾）。 因此算法不能停止在步驟3，所以算法必然停止在步驟2。,.,6/27/2018,87,,令?n+1=?n?{tn/vn}。因?yàn)関n?n=tn?n,所以tn?n/vn??n 令?n+1=?n -{tn?n/vn}。因vn不出現(xiàn)在tn中，所以 于是 故 歸納法完成。即對(duì)所有k≥0,都存在替換?k，使?=?k??k。所以算法終止步驟2時(shí)，?k是W的最一般合一。,,,,.,6/27/2018,88,6.4 一階邏輯中的歸結(jié)原理,,.,6/27/2018,89,,定義（因子） 如果子句C中，兩個(gè)或兩個(gè)以上的文字有一個(gè)最一般合一?，則C?稱(chēng)為C的因子； 如果C?是單元子句，則C?稱(chēng)為C的單因子。 例. C=P(x) ? P(f(y)) ? ～Q(x) 令 ?＝{f(y)/x}，于是 C?= P(f(y)) ? ～Q(f(y)) 是C的因子。,.,6/27/2018,90,二元?dú)w結(jié)式,定義 設(shè)C1, C2是兩個(gè)無(wú)公共變量的子句(稱(chēng)為親本子句), L1, L2分別是C1, C2中的兩個(gè)文字。 如果L1和～L2有最一般合一? ，則子句 (C1?- {L1?}) ? ( C2?- {L2?}) 稱(chēng)為C1和C2的二元?dú)w結(jié)式，L1和L2稱(chēng)為歸結(jié)文字。 例. 設(shè)C1=P(x) ?Q(x), C2=～P(a) ?R(x) 將C2中x改名為y。取L1＝P(x), L2=～P(a), ?={a/x}, 于是(C1?- {L1?}) ? ( C2?- {L2?}) ＝({P(a), Q(a)}-{P(a)}) ? ({～P(a), R(y)}-{～P(a)}) ={Q(a), R(y)}= Q(a)? R(y) ----C1和C2的二元?dú)w結(jié)式.,.,6/27/2018,91,,練習(xí)：設(shè)C1=P(a) ?R(x), C2=～P(y) ?Q(b) 求C1和C2的二元?dú)w結(jié)式.,.,6/27/2018,92,,在謂詞邏輯中，對(duì)子句進(jìn)行歸結(jié)推理時(shí)，要注意 的幾個(gè)問(wèn)題： （1）若被歸結(jié)的子句C1 和C2中具有相同的變?cè)獣r(shí)，需要將其中一個(gè)子句的變?cè)?，否則可能無(wú)法合一，從而沒(méi)有辦法進(jìn)行歸結(jié)。,.,6/27/2018,93,,例： C1=P(x), C2=～P(f(x)) 例：設(shè)知識(shí)庫(kù)中有如下知識(shí)： (1)若x的父親是y，則x不是女人。 (2)若x的母親是y，則x是女人。 (3)Chris的母親是Mary。 (4)Chris的父親是Bill。 求證：這些斷言包含有矛盾。 father(x,y):x的父親是y mother(x,y):x的母親是y woman(x):x是女人,.,6/27/2018,94,,（2）在求歸結(jié)式時(shí),不能同時(shí)消去兩個(gè)互補(bǔ)文字對(duì),消去兩個(gè)互補(bǔ)文字對(duì)所得的結(jié)果不是兩個(gè)親本子句的邏輯推論。 例.設(shè)C1=P(x) ?～Q(b), C2=～P(a) ?Q(y)?R(z) 求C1和C2的二元?dú)w結(jié)式. （3）如果在參加歸結(jié)的子句內(nèi)含有可合一的文字,則在進(jìn)行歸結(jié)之前,應(yīng)對(duì)這些文字進(jìn)行合一,以實(shí)現(xiàn)這些子句內(nèi)部的化簡(jiǎn)。,.,6/27/2018,95,歸結(jié)式,定義 子句C1, C2的一個(gè)歸結(jié)式是下列二元?dú)w結(jié)式之一： C1和C2的二元?dú)w結(jié)式。 C1和C2的因子的二元?dú)w結(jié)式。 C1的因子和C2的二元?dú)w結(jié)式。 C1的因子和C2的因子的二元?dú)w結(jié)式。 例. 設(shè) C1=P(x) ?P(f(y)) ?R(g(y)) C2=～P(f(g(a))) ?Q(b) C1的因子C1’= P(f(y)) ?R(g(y))。于是C1’和C2的二元?dú)w結(jié)式，從而也是C1和C2的歸結(jié)式為 R(g(g(a))) ?Q(b),.,6/27/2018,96,一階邏輯歸結(jié)原理的完備性,提升引理 如果C1’和C2’分別是子句C1和C2的例，C’是C1’和C2’的歸結(jié)式，則存在C1和C2的一個(gè)歸結(jié)式C，使C’是C的例。 例 C1：P(x) ?Q(f(x)) C2： ～Q(y) ?R(y) C1’： P(a) ?Q(f(a)) C2’：～Q(f(a)) ?R(f(a)) C ’： P(a) ? R(f(a)) C： P(x) ?R(f(x)),.,6/27/2018,97,一階邏輯歸結(jié)原理的完備性,定理 若子句集S是不可滿足的，則存在從S推出空子句的歸結(jié)演繹。 證明: 設(shè)子句集S是不可滿足的，由Herbrand定理II知，存在S的一個(gè)基例集S’也是不可滿足的。 根據(jù)命題邏輯歸結(jié)原理的完備性，存在從S’推出空子句的歸結(jié)演繹D’。 由提升引理知，可將D’提升成一個(gè)從S推出空子句的歸結(jié)演繹D。定理得證。,.,6/27/2018,98,,應(yīng)用歸結(jié)原理的習(xí)題,.,6/27/2018,99,6.5 歸結(jié)原理的幾種改進(jìn),,.,6/27/2018,100,,水平浸透法（Level Saturation Method） S0= S Sn= {C1和C2的歸結(jié)式| C1∈S0∪…∪Sn-1，C2 ∈Sn-1},.,6/27/2018,101,例.使用水平浸透法證明 S={P∨Q,～P∨Q, P∨～Q, ～P∨～Q} 不可滿足。,