1、5/12/20221第六章第六章 歸結(jié)原理歸結(jié)原理6.1 子句集的子句集的Herbrand域域 一、一、 Herbrand域與域與 Herbrand解釋解釋l定義（定義（Herbrand域）設(shè)域）設(shè)S為子句集，令為子句集，令H0是出現(xiàn)于是出現(xiàn)于子句集子句集S的常量符號集。如果的常量符號集。如果S中無常量符號出現(xiàn)，中無常量符號出現(xiàn)，則則H0由一個常量符號由一個常量符號a組成。組成。 對于對于i1，2，令，令 Hi = Hi-1 所有形如所有形如f(t1，tn)的項的項 其中其中f(t1，tn)是出現(xiàn)在是出現(xiàn)在S中的所有中的所有n元函數(shù)符號，元函數(shù)符號， tj Hi-1，j1，n 稱稱Hi為為S的

2、的i級常量集，級常量集，H 稱為稱為S的的Herbrand域，域， 簡稱簡稱S的的H域。域。5/12/20222l例例 SP(f(x)，a，g(y)，b) H0 =a, b H1 =a, b, f(a), f(b), g(a), g(b) H2a, 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) 5/12/20223練習(xí)練習(xí): 求S的Herbrand域lSP(x) Q(y)，R(z) lSQ(a) P(f(x)， Q(b) P(g(x,y) 5/12/20224原

3、子集原子集 基例基例l基：把對象中的變量用常量代替后得到的無變量符號出現(xiàn)的對象?；喊褜ο笾械淖兞坑贸Ａ看婧蟮玫降臒o變量符號出現(xiàn)的對象。 基項、基項集、基原子、基原子集合、基文字、基子句、基項、基項集、基原子、基原子集合、基文字、基子句、基子句集基子句集 l定義定義 (原子集、原子集、Herbrand底底) 設(shè)設(shè)S是子句集，形是子句集，形如如P(t1,tn)的基原子集合，稱為的基原子集合，稱為S的的Herbrand底底或或S的原子集的原子集 其中其中P(x1，xn)是出現(xiàn)于是出現(xiàn)于S的所有的所有n元謂詞符號，元謂詞符號，t1，tn是是S的的H域中的元素域中的元素l定義（基例）定義（基例） 設(shè)

4、設(shè)S是子句集，是子句集，C是是S中的一個子中的一個子句用句用S的的H域中元素代替域中元素代替C中所有變量所得到的中所有變量所得到的基子句稱為子句基子句稱為子句C的基例。的基例。5/12/20225練習(xí)練習(xí)l已知已知SP(f(x)，a，g(y)，b)，求，求S的原子集，的原子集， 給給出出P(f(x)，a，g(y)，b)的一個基例。的一個基例。l已知已知SP(x) Q(y)，R(z) ，求求S的原子集，的原子集， 分別給分別給出出P(x) Q(y)， R(z)的所有基例。的所有基例。l已知已知S Q(a) P(f(x)，Q(b) P(g(x,y)， 求求S的的原子集，原子集， 分別給出分別給出Q

5、(a) P(f(x) ， Q(b) P(g(x,y)的一個基例。的一個基例。l設(shè)設(shè)SP(x), Q(f(y) R(y) ，求，求S的的H域，域， S的原子集，的原子集， P(x)的基例的基例, Q(f(y) R(y) 的基例。的基例。5/12/20226H解釋解釋定義（子句集的定義（子句集的H解釋）解釋） 設(shè)設(shè)S是子句集，是子句集，H是是S的的H域，域，I*是是S在在H上上的一個解釋稱的一個解釋稱I*為為S的一個的一個H解釋，如果解釋，如果I*滿足如下條件：滿足如下條件： 1） I*映射映射S中的所有常量符號到自身。中的所有常量符號到自身。 2）若）若f是是S中中n元函數(shù)符號，元函數(shù)符號，h1

6、，hn是是H中元素，則中元素，則I*指定映射：指定映射： (h1，hn) f (h1，hn) 設(shè)設(shè)A=A1，A2，An， 是是S的原子集。于是的原子集。于是S的一個的一個H解釋解釋I可方便地表示為如下一個集合：可方便地表示為如下一個集合： I* m1，m2，mn，其中其中, mi =,T i1,2,. ,FiiiiAAIAAI當(dāng) 被 指定為當(dāng) 被 指定為5/12/20227H解釋的例子例例 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解釋： I1*

7、= 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), 5/12/20228練習(xí)練習(xí)S=P(x)Q(x), P(a), Q(b) ，求S的所有H解釋。5/12/20229二、二、Herbrand解釋與普通解釋的關(guān)系解釋與普通解釋的關(guān)系l子句集子句集S的的H解釋是解釋是S的普通解釋。的普通解釋。lS的普通解釋不一定是的普通解釋不一定是S的的H解釋：普通解釋不解釋：普通解釋不是必須定義在是必須定義在H域上，即使定義在域上，即使定義在H域上，也域上，也不一定是一個不一定是一

8、個H解釋。解釋。l任取普通解釋任取普通解釋I，依照，依照I，可以按如下方法構(gòu)造，可以按如下方法構(gòu)造S的一個的一個H解釋解釋I*，使得若，使得若 S在在 I下為真則下為真則 S在在I*下也為真。下也為真。 5/12/202210例.SP(x), Q(y,f(y,a)令令S的一個解釋的一個解釋I如下：如下： D1，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對應(yīng)于對應(yīng)于I的的H解釋解釋I*： I*P(a), Q(a, a), P(f(a, a),

9、 Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), 5/12/202211例例S=P(x), Q(y, f(y, z)令令S的一個解釋的一個解釋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對應(yīng)對應(yīng)1得得H解釋：解釋：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),

10、 指定指定 a對應(yīng)對應(yīng)2得得H解釋：解釋： 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), 5/12/202212對應(yīng)于對應(yīng)于I的的H解釋解釋I*定義（對應(yīng)于定義（對應(yīng)于I的的H解釋解釋I*） 設(shè)I是子句集S在區(qū)域D上的解釋。H是S的H域。l 是如下遞歸定義的H到D的映射： 1） 若S中有常量符號,H0是出現(xiàn)在S中所有常量符號的集合。 對任意aH0，規(guī)定 (a)=I(a) 若S中無常量符號,H0=a。 規(guī)定 (a)=d,dD。 2）對任意(h1,hn)Hin,及S中任意n元函數(shù)符號f(x

11、1,xn) , 規(guī)定(f(h1，hn) =I(f(h1，hn) 。5/12/202213對應(yīng)于對應(yīng)于I的的H解釋解釋I*l對應(yīng)于對應(yīng)于I的的H解釋解釋I*是如下的一個是如下的一個H解釋：解釋： 任取任取S中中n元謂詞符號元謂詞符號P(x1,xn)， 任取任取(h1,hn) Hn，規(guī)定，規(guī)定 TI*(P(h1，hn)=TI(P(h1 ，hn ) 5/12/202214引理引理 如果某區(qū)域如果某區(qū)域D上的解釋上的解釋I滿足子句集滿足子句集S， 則對應(yīng)于則對應(yīng)于I的任意一個的任意一個H解釋解釋I*也滿足也滿足S。證明：證明：令令S= x1 xn (C1 Cm)，其中，其中Ci為子句為子句（i=1,

12、,m）。由已知）。由已知TI(S)=T，即，即對任意（對任意（x1，xn） Dn，都有，都有TI(Ci（x1，xn）)=T, i=1, ,m5/12/202215因為對因為對S中任意中任意r元謂詞符號元謂詞符號P（x1，xr）和任意（）和任意（h1，hr） Hr，都有，都有TI*( P（h1，hr）)=TI(P（h1 ，hr ）)其中（其中（h1 ，hr ） Dr。所以，對任意（所以，對任意（h1，hn） Hn，都有，都有TI*( Ci（h1，hn）)=TI(Ci（h1 ，hn ）) 其中（其中（h1 ，hn ） Dn。 i=1, ,m。 故對任意（故對任意（h1，hn） Hn ，都有，都有

13、TI*(Ci（h1，hn）)=T, 故故TI*(S)=T，即，即I*滿足滿足S。5/12/202216只考慮子句集的只考慮子句集的H解釋是否夠用？解釋是否夠用？定理定理 子句集子句集S恒假當(dāng)且僅當(dāng)恒假當(dāng)且僅當(dāng)S被其所有被其所有H解釋弄假。解釋弄假。證明證明: 必要性顯然。必要性顯然。充分性。假設(shè)充分性。假設(shè)S被其所有被其所有H解釋弄假，而解釋弄假，而S又是可滿足的。又是可滿足的。設(shè)解釋設(shè)解釋I滿足滿足S，于是由引理知，對應(yīng)于，于是由引理知，對應(yīng)于I的的H解釋解釋I*也滿也滿足足S，矛盾故，矛盾故S是不可滿足的是不可滿足的從現(xiàn)在起，如不特別指出，提到的解釋都是指從現(xiàn)在起，如不特別指出，提到的解釋

14、都是指H解釋解釋 5/12/202217結(jié)論結(jié)論l）子句）子句 C的基例的基例 C被解釋被解釋 I滿足，當(dāng)且僅當(dāng)滿足，當(dāng)且僅當(dāng) C中的一個基文字中的一個基文字L出現(xiàn)在出現(xiàn)在 I中中C= P(x) Q(f(y),a) R(z)C= P(a) Q(f(a),a) R(f(a)5/12/2022182）子句）子句C被解釋被解釋I滿足，當(dāng)且僅當(dāng)滿足，當(dāng)且僅當(dāng) C的每一個基例都被的每一個基例都被I滿足滿足3）子句）子句 C被解釋被解釋 I弄假，當(dāng)且僅當(dāng)弄假，當(dāng)且僅當(dāng) 至少有一個至少有一個C的基例的基例C被被I弄假。弄假。5/12/202219例例.C=P(x) Q(f(x)I1=P(a),Q(a),P(

15、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。 5/12/2022204）子句集）子句集S不可滿足，當(dāng)且僅當(dāng)不可滿足，當(dāng)且僅當(dāng) 對每個解釋對每個解釋I，至少有一個，至少有一個S中某個子句中某個子句C的的基例基例C被被I弄假。弄假。5/12/2022216.2 Herbrand定理定理 Herbrand定理是符號邏輯中一個很重要的定理Herbrand定理

16、就是使用語義樹的方法，把需要考慮無窮個H解釋的問題，變成只考慮有限個解釋的問題5/12/202222一、語義樹l定義定義(互補對互補對) 設(shè)設(shè) A是原子，兩個文字是原子，兩個文字A和和A都是另一個的補，集合都是另一個的補，集合A，A稱為一個互稱為一個互補對補對l定義定義(Tautology,重言式重言式) 含有互補對的子句含有互補對的子句5/12/202223l定義定義 （語義樹）（語義樹） 設(shè)設(shè)S是子句集，是子句集，A是是S的原子集關(guān)于的原子集關(guān)于S的語義樹是一棵向下生長的樹的語義樹是一棵向下生長的樹T在樹的每一節(jié)上都以如下在樹的每一節(jié)上都以如下方式附著方式附著A中有限個原子或原子的否定：中

17、有限個原子或原子的否定： 1）對于樹中每一個節(jié)點）對于樹中每一個節(jié)點N，只能向下引出有限的直接的節(jié)，只能向下引出有限的直接的節(jié) L1，Ln 設(shè)設(shè)Qi是附著在是附著在Li上所有文字的合取，上所有文字的合取，i=1, ,n， 則則Q1 Qn是一個恒真的命題公式是一個恒真的命題公式2）對樹中每一個節(jié)點）對樹中每一個節(jié)點 N，設(shè)，設(shè) I（N）是樹）是樹T由根向下到節(jié)點由根向下到節(jié)點 N 的所有節(jié)上附著文字的并集，的所有節(jié)上附著文字的并集， 則則I（N）不含任何互補對）不含任何互補對語義樹5/12/202224完全語義樹定義（完全語義樹）定義（完全語義樹） 設(shè)設(shè)A=A1,An,是子句集是子句集S的原子集

18、的原子集 S的一個語義樹是完全的，當(dāng)且僅當(dāng)?shù)囊粋€語義樹是完全的，當(dāng)且僅當(dāng) 對于語義樹中每一個尖端節(jié)點對于語義樹中每一個尖端節(jié)點N（即從（即從N不再不再 生出節(jié)的那種節(jié)點），都有生出節(jié)的那種節(jié)點），都有 Ai或或Ai有且僅有一個屬于有且僅有一個屬于I(N),i=1,k,5/12/202225例例. 設(shè)A=P，Q，R是子句集S的原子集，完全語義樹完全語義樹(正規(guī)完全語義樹正規(guī)完全語義樹 )RRRRRRRRQQQQPP5/12/202226Q,RRRQQRRRRRRPPRQP,QQP5/12/202227例. 設(shè)設(shè) S=P(x), Q(f(x)S的原子集為A=P(a), Q(a), P(f(a),

19、Q(f(a), P(f(f(a), Q(f(f(a), P(a)P(a)Q(a)Q(a)P(f(a)Q(a)Q(a)P(f(a)Q(f(a)Q(f(a)5/12/202228語義樹與解釋語義樹與解釋lS的完全語義樹的每一個分枝都對應(yīng)著的完全語義樹的每一個分枝都對應(yīng)著S的一個解釋；的一個解釋；定義（部分解釋）定義（部分解釋）對于子句集對于子句集S的語義樹中的每一個節(jié)點的語義樹中的每一個節(jié)點N,I(N)是是S的某個解釋的子集，稱的某個解釋的子集，稱I(N)為為S的部分解釋。的部分解釋。lS的任意解釋都對應(yīng)著的任意解釋都對應(yīng)著S的完全語義樹中的一條分枝？的完全語義樹中的一條分枝？綜合：綜合： 子句集

20、子句集S的一棵完全語義樹對應(yīng)著的一棵完全語義樹對應(yīng)著S的所有解釋。的所有解釋。5/12/202229證明證明: 若不然，設(shè)若不然，設(shè)T中節(jié)點中節(jié)點N向下生出的向下生出的n個節(jié)個節(jié)L1，Ln的每個節(jié)的每個節(jié)Li上，都至少有一個文字上，都至少有一個文字Ai不在不在I中中由語義樹的定義知：由語義樹的定義知：Q1 Qn是恒真公式是恒真公式,其中其中Qi表示表示Li上所有文字的合取，上所有文字的合取，i=1, , n。將。將Q1 Qn化為合取范式：化為合取范式：Q1 Qn（A1 A2 An） () ()因為每一個析取式中都必須有一個互補對。不妨設(shè)因為每一個析取式中都必須有一個互補對。不妨設(shè)A1A2,于是

21、于是A2,A2都不在都不在I中中,這與這與I是一個解釋矛盾。是一個解釋矛盾。結(jié)論：對結(jié)論：對S的任意解釋的任意解釋I，都可以從，都可以從S的完全語義樹的根點出的完全語義樹的根點出發(fā)，向下找出一條分枝，使該分枝對應(yīng)著解釋發(fā)，向下找出一條分枝，使該分枝對應(yīng)著解釋I。引理引理 設(shè)設(shè)T是子句集是子句集S的完全語義樹，的完全語義樹，I是是S的一個解的一個解釋。于是釋。于是T中任意節(jié)點向下生出的直接節(jié)中，必中任意節(jié)點向下生出的直接節(jié)中，必有一節(jié)，其上所有文字都在有一節(jié)，其上所有文字都在I中。中。5/12/202230子句集的封閉語義樹子句集的封閉語義樹l定義（失效點）定義（失效點） 稱語義樹稱語義樹T中的

22、節(jié)點中的節(jié)點N為失效為失效點，如果點，如果(1)I(N)弄假弄假S中某個子句的某個基例；中某個子句的某個基例；(2)I(N)不弄假不弄假S中任意子句的任意基例，其中中任意子句的任意基例，其中N是是 N的任意祖先節(jié)點。的任意祖先節(jié)點。l定義（封閉語義樹）定義（封閉語義樹） 語義樹語義樹T是封閉的，當(dāng)是封閉的，當(dāng)且僅當(dāng)且僅當(dāng)T的每的每個分枝的終點都是失效點。個分枝的終點都是失效點。l定義（推理點）定義（推理點）稱封閉語義樹的節(jié)點稱封閉語義樹的節(jié)點 N為推理為推理點，如果點，如果N的所有直接下降節(jié)點都是失效點的所有直接下降節(jié)點都是失效點5/12/202231例例. 設(shè)設(shè)S=P, P R, P Q,

23、P R。S的原子集 A=P, Q, RPPQQQQRRRRRRRRPPQQRR5/12/202232練習(xí)練習(xí)l設(shè)子句集S=P(x)Q(x),P(f(x), Q(f(x)分別畫出S的完全語義樹與 封閉語義樹。5/12/202233二、二、Herbrand定理定理Herbrand定理定理I子句集S是不可滿足的，當(dāng)且僅當(dāng)對應(yīng)于S的每一個完全語義樹都存在一個有限的封閉語義樹證明證明: 必要性：若S是不可滿足的，設(shè)T是S的完全語義樹 對T的每一個分枝B,令I(lǐng)B是附著在B上所有文字的集合，則IB是S的一個解釋,故IB弄假S中某子句C的某個基例C由于C是有限的，所以B上存在一個節(jié)點NB使得部分解釋I（NB）

24、弄假C，于是分枝B上存在失效點因此，對T中每一分枝都存在一個失效點，于是從T得到S的一個封閉語義樹T。5/12/202234Herbrand定理定理I子句集S是不可滿足的，當(dāng)且僅當(dāng)對應(yīng)于S的每一個完全語義樹都存在一個有限的封閉語義樹(有限性) 因為封閉語義樹T中每一個節(jié)點只能向下生長有限個節(jié),故T必有有限個節(jié)點.否則,由Konig無限性引理,T中必有一條無窮的分枝,此無窮分枝上當(dāng)然沒有失效點,矛盾。（Konig無限性引理：在一個其點之次數(shù)有限的無限有向樹中，必有一源于根的無限路。 ）充分性：若S的每一個完全語義樹T都對應(yīng)著一個有限封閉語義樹T，則T的每條分枝上都有一個失效點。因為S的任一解釋都

25、對應(yīng)T的某一條分枝，所以每一個解釋都弄假S， 故S是不可滿足的。5/12/202235Herbrand定理定理II 子句集S是不可滿足的，當(dāng)且僅當(dāng)存在S的一個有限不可滿足的S的基例集S。證明證明: 必要性：必要性：若若S恒假，設(shè)恒假，設(shè)T是是S的完全語義樹，由的完全語義樹，由Herbrand定理定理I知，有一個有限封閉知，有一個有限封閉語義樹語義樹 T對應(yīng)著對應(yīng)著T。令令S是被是被 T中所有失效點弄假的所中所有失效點弄假的所有有基例（基例（S中某些子句的基例）的集合。中某些子句的基例）的集合。因為因為T中失效點的個數(shù)有限，所以中失效點的個數(shù)有限，所以S是有限集合。是有限集合。任取任取S的一解釋

26、的一解釋I，則，則I是是S的某個解的某個解釋釋I的子集，而解釋的子集，而解釋I是是T中一個分中一個分枝，所以，枝，所以，I弄假弄假S中子句中子句C，故，故I弄假弄假S。因為。因為I 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)5/12/202236Herbrand定理定理II 子句集S是不可滿足的，當(dāng)且僅當(dāng)存在S的一個有限不可滿足的S的基例集S。充分

27、性：充分性：假設(shè)假設(shè)S有一個有限的不可滿足的基例集有一個有限的不可滿足的基例集S。 任取任取S的解釋的解釋I， 因為因為S的每一個解釋的每一個解釋I都包含著都包含著S的一個解釋的一個解釋I，而而S是不可滿足的，所以是不可滿足的，所以S的任一解釋的任一解釋I都弄假都弄假S，故，故I弄假弄假S中至少一個子句，即中至少一個子句，即I弄假弄假S中至中至少一個子句的基例，亦即少一個子句的基例，亦即I弄假弄假S。 由由I的任意性，知的任意性，知S是不可滿足的。是不可滿足的。5/12/202237 Herbrand定理II提出了一種證明子句集S的不可滿足性的方法：如果存在這樣一個機(jī)械程序，它可以逐次生成S中

28、子句的基例集 S0，Sn，并逐次地檢查S0，Sn，的不可滿足性，那么根據(jù) Herbrand定理，如果 S是不可滿足的，則這個程序一定可以找到一個有限數(shù)N，使SN是不可滿足的。 5/12/202238使用使用Herbrand定理的機(jī)器證明過程定理的機(jī)器證明過程lGilmore過程lD-P過程5/12/202239Gilmore過程（過程（1960年）年）l逐次地生成逐次地生成S0， S1，Sn，其中，其中Si是用是用S的的i級常量集合級常量集合Hi中的常量，代替中的常量，代替S中子句的變量，中子句的變量，而得到的而得到的S的所有基例之集合。的所有基例之集合。l對于每一個對于每一個Si，可以使用命

29、題邏輯中的任意的，可以使用命題邏輯中的任意的方法去檢查方法去檢查Si的不可滿足性。的不可滿足性。 Gilmore使用了所謂乘法方法：即將使用了所謂乘法方法：即將Si化為析取化為析取范式。如果其中任意一個合取項包含一個互補范式。如果其中任意一個合取項包含一個互補對，則可以刪除這個合取項，最后，如果某個對，則可以刪除這個合取項，最后，如果某個Si是空的，則是空的，則Si是不可滿足的。是不可滿足的。l當(dāng)當(dāng)S不可滿足時，該算法一定結(jié)束不可滿足時，該算法一定結(jié)束(半可判定半可判定)。5/12/202240例例. S=P(a), P(x) Q(f(x), Q(f(a) H0=a S0=P(a) (P(a)

30、 Q(f(a) Q(f(a) =(P(a)P(a)Q(f(a)(P(a) Q(f(a)Q(f(a) = =所以，S是不可滿足的。l該算法具有指數(shù)復(fù)雜性，為此提出了改進(jìn)規(guī)則，稱為該算法具有指數(shù)復(fù)雜性，為此提出了改進(jìn)規(guī)則，稱為Davis-Putnam預(yù)處理預(yù)處理-檢驗基子句集不可滿足性。檢驗基子句集不可滿足性。5/12/202241D-P過程過程設(shè)設(shè)S是基子句集是基子句集lTautology刪除規(guī)則刪除規(guī)則 設(shè)設(shè)S為刪去為刪去S中所有的中所有的Tautology所剩子句集，所剩子句集， 則則 S恒假恒假 iff S恒假。恒假。 5/12/202242l單文字規(guī)則單文字規(guī)則 若若S中有一個單元基子句

31、中有一個單元基子句L，令令S為刪除為刪除S中包含中包含L的所有基子句所剩子句集，的所有基子句所剩子句集，則：則：(1) 若若S為空集，則為空集，則S可滿足?？蓾M足。(2) 否則，否則， 令令S為刪除為刪除S中所有文字中所有文字L所得子句集所得子句集 （若（若S 中有單元基子句中有單元基子句L，則刪文字，則刪文字L 得空子句），得空子句）， 于是，于是， S恒假恒假 iff S恒假。恒假。S=L(LC1) (LCi) (LCi+1) (LCj) Cj+1 Cn5/12/202243定義（純文字）：稱定義（純文字）：稱S的基子句中文字的基子句中文字L是純的，如果是純的，如果L不出現(xiàn)在不出現(xiàn)在S中。

32、中。l純文字規(guī)則純文字規(guī)則設(shè)設(shè)L是是S中純文字，且中純文字，且S為刪除為刪除S中所有包含中所有包含L的基子句所的基子句所剩子句集，則剩子句集，則(1)若若S為空集，則為空集，則S可滿足?？蓾M足。(2) 否則，否則，S恒假恒假 iff S恒假。恒假。S=(LC1) (LCi) Ci+1 Cn5/12/202244l分裂規(guī)則分裂規(guī)則若若S=(A1 L) (Am L) (B1 L) (Bn L) R 其中其中A i , Bi ,R都不含都不含L或或L，令，令 S1 =A1 Am RS2= B1 Bn R 則則S恒假恒假 iff S1 ， S2同時恒假。同時恒假。 5/12/202245Davis-P

33、utnam方法練習(xí)方法練習(xí)lS= (P Q R) (P Q) P R UlS= (P Q) (P Q) (Q R) (Q R) lS= (P Q) (P Q) (R Q) (R Q) 5/12/202246Herbrand定理的主要障礙定理的主要障礙l要求生成關(guān)于子句集要求生成關(guān)于子句集S的基例集的基例集 S1, S2, 。在多數(shù)情。在多數(shù)情況下，這些集合的元數(shù)是以指數(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,

34、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個元素個元素 S5是不可滿足的，但是是不可滿足的，但是H5是是1065數(shù)量級個元素，而數(shù)量級個元素，而S5有有10260數(shù)量級的元素。想將數(shù)量級的元素。想將S5存儲起來都是不可能的，存儲起來都是不可能的，更不要說是檢查它的不可滿足性了。更不要說是檢查它的不可滿足性了。5/12/202247l為了避免像Herbrand定理所要求的那樣去生成子句的基例集，J.A.Robinson于

35、1965年提出了歸結(jié)原理，歸結(jié)原理可以直接應(yīng)用到任意子句集S上（不一定是基子句集），去檢查S的不可滿足性。l歸結(jié)原理的本質(zhì)思想是去檢查子句集S是否包含一個空子句: 如果S包含，則S是不可滿足的。 如果S不包含，則去檢查是否可由S推導(dǎo)出來。 當(dāng)然這個推理規(guī)則必須保證推出的子句是原親本子句的邏輯結(jié)果。歸結(jié)原理就是具有這種性質(zhì)的一種推理規(guī)則。 歸結(jié)原理思想歸結(jié)原理思想5/12/202248命題邏輯中的歸結(jié)原理命題邏輯中的歸結(jié)原理5/12/202249歸結(jié)式歸結(jié)式l定義（定義（歸結(jié)式） 對任意兩個基子句C1和C2。如果C1中存在文字L1，C2中存在文字L2，且L1L2， 則從C1和C2中分別刪除L1和

36、L2，將C1和C2的剩余部分析取起來構(gòu)成的子句，稱為C1和C2的歸結(jié)式，記為R(C1, C2)。 C1和C2稱為親本子句。5/12/202250練習(xí)練習(xí):求下述各子句對的歸結(jié)式求下述各子句對的歸結(jié)式 lC1= PQR, C2=QSlC1= PQR, C2=P RQ5/12/202251定理定理 設(shè)C1和C2是兩個基子句， R(C1, C2) 是C1，C2的歸結(jié)式，則R(C1, C2)是C1和C2的邏輯結(jié)果。證明：證明： 設(shè) C1=L C1, C2=LC2。于是 R(C1, C2) C1 C2 設(shè)I是C1和C2的一個解釋，且滿足C1也滿足C2。因為L和L中有一個在I下為假，不妨設(shè)為L。于是C1非

37、空，且在I下為真。故R(C1, C2)在I下為真。 命題邏輯歸結(jié)方法的可靠性命題邏輯歸結(jié)方法的可靠性5/12/202252歸結(jié)演繹歸結(jié)演繹l定義（歸結(jié)演繹）定義（歸結(jié)演繹） 設(shè)設(shè)S是子句集。從是子句集。從S推出子句推出子句C的一個歸的一個歸結(jié)演繹是如下一個有限子句序列：結(jié)演繹是如下一個有限子句序列： C1，C2，Ck其中其中Ci或者是或者是S中子句，或者是中子句，或者是Cj和和Cr的歸結(jié)式的歸結(jié)式 (j i, r i)；并且并且CkC。 稱從子句集稱從子句集S演繹出子句演繹出子句C，是指存在一個從，是指存在一個從S推出推出C的演繹。的演繹。l定理定理 若從子句集若從子句集S可以演繹出子句可以演

38、繹出子句C，則，則C是是S的邏輯結(jié)果。的邏輯結(jié)果。l推論推論 若子句集若子句集S是可滿足的，是可滿足的， 則則S推出的任意子句也是可滿足的。推出的任意子句也是可滿足的。 5/12/202253定義定義 從從S推出空子句的演繹稱為一個推出空子句的演繹稱為一個反駁（反駁（反反證證） ，或稱為，或稱為S的一個證明。的一個證明。結(jié)論結(jié)論：若從基子句集：若從基子句集S可演繹出空子句，則可演繹出空子句，則S是是不可滿足的。不可滿足的。演繹樹：演繹樹：從子句集從子句集S出發(fā)，通過歸結(jié)原理可得到出發(fā)，通過歸結(jié)原理可得到一個向下的演繹樹，其每個初始節(jié)點上附著一一個向下的演繹樹，其每個初始節(jié)點上附著一個個S中子句

39、，每個非初始節(jié)點上附著一個其前中子句，每個非初始節(jié)點上附著一個其前任節(jié)點上子句的歸結(jié)式。任節(jié)點上子句的歸結(jié)式。5/12/202254例. S=P Q, P Q, P Q, P Q 歸結(jié)演繹： (1) PQ (2) PQ (3) PQ (4) PQ (5) Q 由(1)、(2) (6) Q 由(3)、(4) (7) 由(5)、(6)5/12/202255歸結(jié)原理歸結(jié)原理一般過程一般過程:1)建立子句集S。2)如果S含空子句，則結(jié)束。3)從子句集S出發(fā),僅對S的子句間使用歸結(jié)推理規(guī)則。4)如果得出空子句，則結(jié)束。5)將所得歸結(jié)式仍放入S中。6)對新的子句集使用歸結(jié)推理規(guī)則。轉(zhuǎn)4)。5/12/202

40、256例例.證明證明(P Q) Q p首先建立子句集:S=PQ, Q , P歸結(jié)演繹:(1) P Q(2) Q(3) P(4) P (1)(2)歸結(jié)(5) (3)(4)歸結(jié)5/12/202257命題邏輯歸結(jié)原理的完備性命題邏輯歸結(jié)原理的完備性l定理 如果基子句集如果基子句集S是不可滿足的，是不可滿足的， 則存在從則存在從S推出空子句的歸結(jié)演繹。推出空子句的歸結(jié)演繹。證明： 設(shè)M是S的原子集，對M的元素數(shù)|M|用歸納法。 當(dāng)|M|=1時，設(shè)原子為P。 若S ，得證。 否則，因為S是不可滿足的，于是，S中必包含單元子句P和P，而P和P的歸結(jié)式是，所以存在從S推出的歸結(jié)演繹。 假設(shè)|M|n (n2)

41、 時，定理成立。往證 |M|n時定理成立。 5/12/202258取取M中任意一原子中任意一原子P，做如下兩個子句集：，做如下兩個子句集：S：將將S中所有含中所有含P的子句刪除，然后在剩下的子的子句刪除，然后在剩下的子 句中刪除文字句中刪除文字P；S”：將：將S中所有含中所有含P的子句刪除，然后在剩下的的子句刪除，然后在剩下的 子句中刪除文字子句中刪除文字P。顯然，顯然，S和和S”都不可滿足，且它們的原子集的元都不可滿足，且它們的原子集的元素數(shù)都小于素數(shù)都小于n。根據(jù)歸納假設(shè)，存在從。根據(jù)歸納假設(shè)，存在從S推出推出 的的歸結(jié)演繹歸結(jié)演繹D1，從，從S”推出推出的歸結(jié)演繹的歸結(jié)演繹D2。5/12

42、/202259lS=PC1, ,PCi , PCi+1, ,PCj, Cj+1 , , CnS=Ci+1, ,Cj,Cj+1 , , CnS=C1, ,Ci , Cj+1 , , Cnl例：S=P Q, P Q, P R, RM=P,Q,R5/12/202260 在在D1中，將中，將S中所有不是中所有不是S中的子句，通過中的子句，通過添加文字添加文字P而恢復(fù)成而恢復(fù)成S中子句，于是，得到從中子句，于是，得到從S推出推出 或者或者P的歸結(jié)演繹的歸結(jié)演繹D1。 用同樣方法從用同樣方法從D2可得一個從可得一個從S推出推出 或者或者P的的歸結(jié)演繹歸結(jié)演繹D2。 顯然，從顯然，從D1和和D2就不難得到一

43、個從就不難得到一個從S推出推出 的的歸結(jié)演繹歸結(jié)演繹D。歸納法完成。歸納法完成。5/12/202261Resolution Principle 兩種譯法：歸結(jié)原理：從內(nèi)部看 劉敘華，一種新的語義歸結(jié)原理，吉林大學(xué)學(xué)報，1978。消解原理：從外部看 馬希文，機(jī)器證明及其應(yīng)用，計算機(jī)應(yīng)用， 1978。5/12/2022626.3 合一算法合一算法5/12/202263例例1 C1：P(x) Q(y) C2：P(a) R(z)例例2 C1：P(x) Q(x) C2：P(f(x) R(x)l替換和合一是為了處理謂詞邏輯中子句之間的模式匹配而引進(jìn).5/12/202264一、替換與最一般合一替換一、替換與

44、最一般合一替換l定義定義(替換替換)一個替換是形如一個替換是形如t1/v1, , tn/vn 的一個有限集合，其中的一個有限集合，其中vi是變量符號，是變量符號，ti是不是不同于同于vi的項。并且在此集合中沒有在斜線符的項。并且在此集合中沒有在斜線符號后面有相同變量符號的兩個元素，稱號后面有相同變量符號的兩個元素，稱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)當(dāng)t1,tn是基項時，稱此替換為基替換。是基項時，

45、稱此替換為基替換。空替換：空替換：沒有元素的替換稱為空替換，記為沒有元素的替換稱為空替換，記為 。5/12/202265替換定義（改名）定義（改名） 設(shè)替換設(shè)替換 = t1/x1, , tn/xn 如果如果t1, , tn是不同的變量符號，則稱是不同的變量符號，則稱 為一個改為一個改名替換，簡稱改名。名替換，簡稱改名。替換作用對象：替換作用對象：表達(dá)式表達(dá)式（項、項集、原子、原子集、（項、項集、原子、原子集、 文字、子句、子句集）文字、子句、子句集）基表達(dá)式：基表達(dá)式：沒有變量符號的表達(dá)式。沒有變量符號的表達(dá)式。子表達(dá)式：子表達(dá)式：出現(xiàn)在表達(dá)式出現(xiàn)在表達(dá)式E中的表達(dá)式稱為中的表達(dá)式稱為E的子的

46、子 表達(dá)式。表達(dá)式。5/12/202266E的例l 定義（定義（E的例）的例） 設(shè)設(shè) = t1/v1, , tn/vn 是一個是一個替換，替換，E是一個表達(dá)式。將是一個表達(dá)式。將E中出現(xiàn)的每一個中出現(xiàn)的每一個變量符號，變量符號，vi (1 i n) ，都用項，都用項ti替換，這樣替換，這樣得到的表達(dá)式記為得到的表達(dá)式記為E 。稱。稱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)5/12/20226

47、7練習(xí)：l E=P(x, g(y), h(x,z), =a/x, f(b)/y, g(w)/zE=P(a, g(f(b), h(a,g(w)l E=P(x, y, z), =y/x, z/y E=P(y, z, z). EP(z, z, z). 5/12/202268替換的乘積替換的乘積 l定義（替換的乘積）定義（替換的乘積）設(shè)設(shè) = t1/x1, , tn/xn ， = u1/y1, , um/ym 是兩個替換。將下面集合是兩個替換。將下面集合 t1 /x1, , tn /xn , u1/y1, , um/ym 中任意符合下面條件的元素刪除：中任意符合下面條件的元素刪除： 1）ui/yi，當(dāng)

48、，當(dāng)yi x1, , xn 時；時； 2）ti /xi，當(dāng)，當(dāng)ti = xi 時。時。如此得到一個替換，稱為如此得到一個替換，稱為 與與 的乘積，記為的乘積，記為 。l例例. 令令 =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 5/12/202269=a/x, =b/x =a/x =b/x可見： 5/12/202270 例子例子: E=P(x, y, z) =a/x, f(z)/

49、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)5/12/202271引理引理 若若E是表達(dá)式，是表達(dá)式， ， 是兩個替換，是兩個替換， 則則E ( ) = (E ) 證明：證明： 設(shè)設(shè)vi是是E中任意一個變量符號，而中任意一個變量符號，而 = t1/x1, , tn/xn ， = u1/y1, , um/ym l若若vi既不在既不在 x1, , xn 中，也不在中，也不在 y1, , ym 中，則中，則vi在在E ( )中和在中和在(

50、E ) 中都不變。中都不變。l若若vi=xj (1 j n)，則，則E中的中的vi，在，在(E ) 中先變成中先變成tj，然后，然后再變成再變成tj ；E中的中的vi在在E()中立即就變成了中立即就變成了tj 。故。故E中中vi在在(E ) 中和在中和在E()中有相同變化。中有相同變化。l若若vi=yj (1 j m)，且，且yj x1,xn ，則，則E中中vi在在(E ) 中中變?yōu)樽優(yōu)閡j;E中中vi在在E()中也變?yōu)橹幸沧優(yōu)閡j(注意注意:yj x1, xn，所，所以以uj/yj），故），故E中中vi在在(E ) 中和在中和在E ()中有相同變中有相同變化?；?。 由于由于vi的任意性，故引

51、理得證。的任意性，故引理得證。 5/12/202272引理引理 設(shè)設(shè) ， ， 是三個替換，是三個替換， 于是于是() ()證明：證明： 設(shè)設(shè)E是任一表達(dá)式，由上面引理知是任一表達(dá)式，由上面引理知 E() =(E() = (E ) ) E( () =(E ) () = (E ) ) 所以所以 E() = E( ()由于由于E的任意性，故的任意性，故 () ()5/12/202273l定義定義(合一合一)稱替換稱替換 是表達(dá)式集合是表達(dá)式集合E1,Ek的的 合一，當(dāng)且僅當(dāng)合一，當(dāng)且僅當(dāng)E1 E2 =Ek 。 表達(dá)式集合表達(dá)式集合E1, , Ek稱為可合一的，如稱為可合一的，如果存在關(guān)于此集合的一個

52、合一。果存在關(guān)于此集合的一個合一。l定義定義(最一般合一最一般合一) 表達(dá)式集合表達(dá)式集合E1, , Ek的合一的合一 稱為是最一般合一稱為是最一般合一(most general unifier, 簡寫為簡寫為mgu)，當(dāng)且僅當(dāng)對此集合的每，當(dāng)且僅當(dāng)對此集合的每一個合一一個合一 ，都存在替換，都存在替換 ，使得，使得 5/12/202274l例例. 表達(dá)式集合P(a, y), P(x, f(b)是可合一的，其最一般合一a/x, f(b)/y。顯然，這也是此集合的mgu。？ 表達(dá)式集合P(a, b), P(x, f(b)是否可合一？l例例. 表達(dá)式集合P(x), P(f(y)是可合一的，其最一般

53、合一f(y)/x f(a)/x, a/y也是合一，有替換 =a/y，使=f(y)/xa/y5/12/202275l例例 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/x5/12/202276二、二、合一算法合一算法定義（差異集合）定義（差異集合） 設(shè)W是非空表達(dá)式集合，W的差異集合是如下一個集合：首先找出W的所有表達(dá)式中不是都相同的第一個符號，然后從W的每一個表達(dá)式中抽出占有這個符號位置的子表達(dá)式。所有這些子表達(dá)式組成的集合稱為這步找到的W的差異集合D。5

54、/12/202277W不可合一的三種情況不可合一的三種情況（1）若D中無變量符號為元素，則W是不可合一的。l例例. W=P(f(x), P(g(x) D=f(x), g(x) （2）若D中有奇異元素和非奇異元素，則W是不可合一的。l例例. W=P(x), P(x, y) D=, y（3）若D中元素有變量符號x和項t，且x出現(xiàn)在t中，則W是不可合一的。l例例. W=P(x), P(f(x) D=x, f(x)5/12/202278l換名換名:P(f(x), x), P(x, a);如果不換名：D=f(x), x.換名: P(f(y), y), P(x, a);mgu: f(a)/x, a/y5/

55、12/202279步驟1：置 k=0, Wk=W, k=步驟2：若Wk只有一個元素，則停止，k是W的最一般合一； 否則，找出Wk的差異集合Dk。步驟3：若Dk非奇異，Dk中存在元素vk和tk，其中vk是變量符號，并且 不出現(xiàn)在tk中，則轉(zhuǎn)步驟4； 否則，算法停止，W是不可合一的。步驟4：令 k+1=ktk/vk，Wk+1=Wk （注：Wk+1=W ）步驟5：置 k=k+1，轉(zhuǎn)步驟2。合一算法（合一算法（Unification algorithm） /kkvt1k5/12/202280例例. 令 W=Q(f(a), g(x), Q(y, y), 求W的mgu。l步驟1： k=0, W0=W, 0

56、=。l步驟2： D0 =f(a), y。l步驟3：有v0= y D0，v0不出現(xiàn)在t0f(a)中。l步驟4：令 1=0t0/v0=f(a)/y, W1=Q(f(a), g(x), Q(f(a), f(a)l步驟5：k=k+1=1l步驟2： D1 =g(x), f(a) 。l步驟3：D1中無變量符號，算法停止，W不可合一。？ 若令W=Q(f(a), g(x), Q(y, z), W是否可合一？5/12/202281例例 令令 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

57、= z D0，v0不出現(xiàn)在t0a中。步驟4：令 1=0t0/v0=a/z=a/z，W1=W0t0/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)在t1f(a)中。步驟4：令 2=1t1/v1=a/z f(a)/x =a/z, f(a)/x ，W2=W1t1/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)5/12/202282例例.步驟步驟5：

58、k=k+1=2步驟步驟2： D2 =g(y), u。步驟步驟3：有：有v2= u D2，且，且v2不出現(xiàn)在不出現(xiàn)在t2g(y)中。中。步驟步驟4：令：令 3= 2 t2/v2=a/z, f(a)/x g(y)/u =a/z, f(a)/x, g(y)/u ，W3=W2t2/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只有一個元素。算法停止。只有一個元素。算法停止。 3=a/z, f(a)/x, g(y)/u 是是W的最一般合一。的最一般合一。5/12/202283定理定理

59、 若若W是關(guān)于表達(dá)式的是關(guān)于表達(dá)式的有限非空可合一有限非空可合一集合，則合一集合，則合一算法終將結(jié)束在步驟算法終將結(jié)束在步驟2，并且最后的，并且最后的 k是是W的最一般合一。的最一般合一。證明： （1）終止性。否則將產(chǎn)生一個無窮序列：W ， W ， W ，其中每一個直接后繼集合比它的前任都少一個變量符號（注意：W 包含vk，而W 不包含vk）。但這是不可能的，因為W僅含有限個變量符號。 （2） k是W的合一。若算法停止在步驟2，則Wk=W只含有一個元素，所以k是W的合一。01nk1k5/12/202284（3）用歸納法證明算法必不會停止在步驟用歸納法證明算法必不會停止在步驟3，并，并且對任意且

60、對任意W的一個合一的一個合一 ，任意，任意k，都存在替換，都存在替換 k，使得，使得 = kk 亦即亦即 k是是W的的mgu。 當(dāng)當(dāng)k=0時，因時，因 0= ，取，取 0= ，于是，于是 = 00。5/12/202285假設(shè)對假設(shè)對0 k n， = kk成立。成立。 往證：存在往證：存在 n+1，使得，使得 = n+1n+1。若若W 只含有一個元素，則合一算法結(jié)束在步驟只含有一個元素，則合一算法結(jié)束在步驟2。因為。因為 = nn，且，且 n是是W的合一，故的合一，故 n是是W的的mgu。定理得證。定理得證。 若若W 不只含有一個元素不只含有一個元素,按照算法按照算法,將找出將找出W的差異集合的