人工智能謂詞邏輯與歸結原理課件

人工智能謂詞邏輯與歸結原理人工智能謂詞邏輯與歸結原理人工智能謂詞邏輯與歸結原理第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理命題邏輯基礎命題邏輯基礎：定義：合取式：p與q，記做p∧

q析取式：

p或q，記做p∨

q蘊含式：如果p則q，記做p→

q等價式：p當且僅當q，記做p<=>

q

……命題邏輯基礎定義：若A無成假賦值，則稱A為重言式或永真式；若A無成真賦值，則稱A為矛盾式或永假式；若A至少有一個成真賦值，則稱A為可滿足的；析取范式：僅由有限個簡單合取式組成的析取式。合取范式：僅由有限個簡單析取式組成的合取式。命題邏輯基礎基本等值式24個(1)交換率：p∨q<=>q

∨p

；

p∧q<=>q∧

p

結合率：(p∨q)∨

r<=>p∨(q∨r);

(p∧

q)

∧

r<=>p∧(q∧

r)分配率：p∨(q∧

r)<=>(p∨q)

∧(p∨r)

；

p∧(q∨

r)<=>(p∧

q)

∨(p∧

r)

命題邏輯基礎基本等值式（1）摩根率:～

(p∨q)

<=>～

p∧

～

q

；

～

(p∧

q)

<=>～

p∨

～

q

吸收率:p∨(p∧

q)<=>p

；

pΛ(p∨q)<=>p

同一律:p∨0

<=>p

；

p∧1

<=>p

蘊含等值式:p→

q

<=>～

p∨q

假言易位式:p→

q

<=>～p→～

q

命題例命題：能判斷真假（不是既真又假）的陳述句。

簡單陳述句描述事實、事物的狀態(tài)、關系等性質。例如：1．

1+1=22．

雪是黑色的。3．

北京是中國的首都。4．

到冥王星去渡假。

命題例判斷一個句子是否是命題，有先要看它是否是陳述句，而后看它的真值是否唯一。以上的例子都是陳述句，第4句的真值現(xiàn)在是假，隨著人類科學的發(fā)展，有可能變成真，但不管怎樣，真值是唯一的。因此，以上4個例子都是命題。而例如：1．

快點走吧！

2．

到那去？

3．

x+y>10

等等句子，都不是命題。命題表示公式（1）將陳述句轉化成命題公式。如：設“下雨”為p，“騎車上班”為q，，1．“只要不下雨，我騎自行車上班”?！玴

是q的充分條件， 因而，可得命題公式：～p→q2．“只有不下雨，我才騎自行車上班”。～p

是q的必要條件， 因而，可得命題公式：q→～p命題表示公式（2）例如：1．

“如果我進城我就去看你，除非我很累?！? 設：p，我進城，q，去看你，r，我很累。 則有命題公式：～r→(p→q)。2．“應屆高中生，得過數(shù)學或物理競賽的一等獎， 保送上北京大學。” 設：p，應屆高中生，q，保送上北京大學上學，

r，是得過數(shù)學一等獎。t，是得過物理一等獎。 則有命題公式公式：p

∧(r∨t)→

q。

命題邏輯的推理自然演繹推理自然演繹推理：從一組已知為真的事實出發(fā)，直接運用經(jīng)典邏輯推理的推理規(guī)則推出結論的過程?；疽?guī)則

P規(guī)則：在推理的任何步驟上都可以引入前提。T規(guī)則：在推理時，如果前面步驟有一個或多個公式永真蘊含公式S，則可以把S引入推理中。假言推理：若P,PQ為真，則Q為真。拒取式：若PQ,Q為真，則P為假。析取三段論：若P,P∨Q為真，則Q為真。命題邏輯的推理證明：如果今天是下雨天，則帶傘或雨衣。如果走路上班，則不帶雨衣。今天下雨，走路上班，所以帶傘。設P--今天下雨，Q--帶傘，R--帶雨衣，S--走路上班。前提：P(Q∨R),SR,P,S結論：

QP(Q∨R)P規(guī)則P

P規(guī)則(Q∨R)假言推理SRP規(guī)則SP規(guī)則R假言推理Q析取三段論

謂詞邏輯基礎命題：能分辨其真假的語句。謂詞邏輯：用謂詞來表示命題。個體詞：表示思維對象的詞，有個體常項和個體變項。謂詞：表示個體詞的性質或多個個體詞之間的關系的詞。有n個個體詞的謂詞P(x1,x2,x3,…)稱為n元謂詞。 函數(shù)：表示從個體域到另一個體域的映射。謂詞邏輯基礎量詞：對個體詞數(shù)量上的限制，只討論全稱量詞和存在量詞

。聯(lián)結詞：為了表現(xiàn)更復雜的內容，聯(lián)結各簡單謂詞公式構成復合謂詞公式的詞。有∨

謂詞邏輯基礎合式公式：單個謂詞是合式公式，成為原子謂詞公式。若A是合式公式，則A也是合式公式。若A，B是合式公式，則AB,A∨B,AB,AB也是合式公式。若A是合式公式，x是任一個體變元，則(x)A和(x)A也是合式公式。 謂詞邏輯基礎謂詞公式的等價式

交換律PQQP,P∨QQ∨P 分配律P∨(QR)(P∨Q)(P∨R)狄摩根律(PQ)

P∨

Q,(P∨Q)

P

Q

雙重否定律

QQ連接詞化歸律PQ

P∨Q量詞轉化律(x)P(x)(P)，(x)P(x)(

P)一階謂詞邏輯知識表示方法一階謂詞邏輯是謂詞邏輯中最直觀的一種邏輯。它以謂詞形式來表示動作的主體、客體?？腕w可以多個。

如：張三與李四打網(wǎng)球（ZhangandLiplaytennis），可寫為：play(Zhang,Li,tennis)

這里謂詞是play，動詞主體是Zhang和Li，而客體是tennis。謂詞邏輯規(guī)范表達式：

P(x1,x2,x3,…)，這里P是謂詞,xi是主體與客體。一階謂詞邏輯知識表示方法例：王的職業(yè)為教師。設謂詞P(x,a)

P(Wang,Teacher)所有男性年齡大于60歲則退休。設謂詞A(y,b),G(x,y),S(z,c),R(t)

(u){S(u,male)(x)[A(u,x)G(x,60)]R(u)}一階謂詞邏輯知識表示方法謂詞比命題更加細致地刻畫知識：表達能力強如：北京是個城市，City(x)

把城市這個概念分割出來。把“城市”與“北京”兩個概念連接在一起，而且說明“北京”是“城市”的子概念。（有層）謂詞可以代表變化的情況如：City(北京),真。City(煤球)，假在不同的知識之間建立聯(lián)系……….一階謂詞邏輯知識表示方法在不同的知識之間建立聯(lián)系如：Human(x)→Lawed(x)，人人都受法律管制，x是同一個人。

Commit(x)→Punished(x)，x犯了罪就一定要受到懲罰。 而，{[Human(x)→Lawed(x)]→[commit(x)→Punished(x)]}， 意為如果由于某個x是人而受法律管制，則這個人犯了罪就一定要受到懲罰。一階謂詞邏輯知識表示方法例：兔子F(x)比烏龜G(y)跑得快H(x,y)(x)(y)(F(x)G(y)H(x,y))有的兔子比所有烏龜跑得快

(x)F(x)(y)(G(y)H(x,y))并不是所有的兔子都比烏龜跑得快

(x)(y)(F(x)G(y)H(x,y))不存在跑得一樣快L(x,y)的兩子兔子

(x)(y)(F(x)G(y)L(x,y))一階謂詞邏輯知識表示方法謂詞邏輯表示法在實際人工智能系統(tǒng)上得到應用。機器人行動（如圖示）1.引入謂詞

Table(x):x是桌子

Empty(y):y手中為空

At(y,z):y在z附近

Holds(y,w):y拿著wOn(w,x):w在x的上面

cab一階謂詞邏輯知識表示方法機器人行動初始狀態(tài)S0

目標狀態(tài)Sg

At(robot,c)Empty(robot)On(box,a)Table(a)Table(b)At(robot,c)Empty(robot)On(box,b)Table(a)Table(b)一階謂詞邏輯知識表示方法機器人行動2.引入算子（狀態(tài)轉移函數(shù)）

Goto(x,y):從x處走到y(tǒng)處

Pick_up(x):在x處拿起盒子

Set_down(x):在x處放下盒子

一階謂詞邏輯知識表示方法3.問題描述

At(robot,c)Empty(robot)On(box,a)Table(a)Table(b)At(robot,a)Empty(robot)On(box,a)Table(a)Table(b)At(robot,a)Holds(robot,box)Table(a)Table(b)Goto(x,y)Pick_up(x)一階謂詞邏輯知識表示方法3.問題描述

At(robot,b)Holds(robot,box)Table(a)Table(b)At(robot,b)Empty(robot)On(box,b)Table(a)Table(b)At(robot,c)Empty(robot)On(box,b)Table(a)Table(b)Set_down(x)Goto(x,y)Goto(x,y)一階謂詞邏輯知識表示方法

“猴子吃香蕉”問題的描述1.引入謂詞

P(x,y,z,s):猴子在x處，香蕉在y處，梯子在z處，相應狀態(tài)為s。

R(s):在s狀態(tài)下猴子吃到香蕉。2.引入算子

Wolk(y,z,s):在原狀態(tài)s下，猴子從y處走到z處，建立新狀態(tài)。

Carry(y,z,s):在原狀態(tài)s下，猴子推梯子從y處到z處，建立新狀態(tài)。

Climb(s):在原狀態(tài)s下，猴子爬上梯子。3.問題描述……一階謂詞邏輯知識表示方法

“猴子吃香蕉”問題的描述3.問題描述……A1(x)(y)(z)(s)(P(x,y,z,s)P(z,y,z,Walk(x,z,s)))A2(x)(y)(s)(P(x,y,x,s)P(y,y,y,Carry(x,y,s)))A3(s)(P(b,b,b,s)R(Climb(s)))A4P(a,b,c,s)A5R(s)∨ANS(s)一階謂詞邏輯知識表示方法謂詞邏輯法是應用最廣的方法之一，其原因是：謂詞邏輯與數(shù)據(jù)庫，特別是關系數(shù)據(jù)庫就有密切的關系。在關系數(shù)據(jù)庫中，邏輯代數(shù)表達式是謂詞表達式之一。因此，如果采用謂詞邏輯作為系統(tǒng)的理論背景，則可將數(shù)據(jù)庫系統(tǒng)擴展改造成知識庫。

一階謂詞邏輯具有完備的邏輯推理算法。如果對邏輯的某些外延擴展后，則可把大部分的知識表達成一階謂詞邏輯的形式。（知識易表達）………..一階謂詞邏輯知識表示方法謂詞邏輯法是應用最廣的方法之一，其原因是：………..謂詞邏輯本身具有比較扎實的數(shù)學基礎，知識的表達方式?jīng)Q定了系統(tǒng)的主要結構。因此，對知識表達方式的嚴密科學性要求就比較容易得到滿足。這樣對形式理論的擴展導致了整個系統(tǒng)框架的發(fā)展。

邏輯推理是公理集合中演繹而得出結論的過程。由于邏輯及形式系統(tǒng)具有的重要性質，可以保證知識庫中新舊知識在邏輯上的一致性（或通過相應的一套處理過程檢驗）、和所演繹出來的結論的正確性。而其它的表示方法在這點上還不能與其相比。謂詞邏輯基礎模式匹配（置換與合一）什么叫模式匹配：是指對兩個知識模式（謂詞公式、框架片斷、語義網(wǎng)絡片斷等）的比較與耦合，即檢查這兩個知識模式是否完全一致或近似一致。模式匹配有確定性匹配與不確定性匹配。什么叫合一：一個表達式（公式）的項可以是常量、變量或函數(shù)，合一就是尋找項對變量的置換而使得表達式（公式）一致的過程。合一是AI中很重要的過程。

基本概念模式匹配（置換與合一）置換：有序對的集合S={t1/x1,t2/x2,…,tn/xn}

表示置換。其中ti/xi表示在公式中用ti代替xi

。例：公式P[x,f(y),B]s1={z/x,w/y}則P[z,f(w),B]s2={A/y}則P[x,f(A),B]s3={g(z)/x}則P[g(z),f(y),B]用置換s作用于公式E所得到的式子記為Es

基本概念模式匹配（置換與合一）置換的復合：設有={t1/x1,t2/x2,…,tn/xn}

和={u1/y1,u2/y2,…,un/yn}是兩個置換。則兩個置換的復合也是一個置換。={t1/x1,t2/x2,…,tn/xn，u1/y1,u2/y2,…,um/ym}

其中ti

xi

并且yi{x1,x2,…,xn}

例：

s1={g(x,y)/z,u/w}s2={A/x,B/y,C/w,D/z,w/u}

則s1s2={g(A,B)/z,A/x,B/y,w/u}性質：滿足結合律，而不滿足交換律（1）2=（12），而一般1221

基本概念模式匹配（置換與合一）可合一：設有公式集合F={F1,F2,…,Fn},若存在一個置換使得

F1=F2=…=Fn

，則稱公式集F是可合一的。稱為公式集F的一個合一。例：F={P[x,f(y),B],P[x,f(B),B]}

則s1={A/x,B/y}是公式集F的一個合一

s2={B/y}也是公式集F的一個合一

基本概念模式匹配（置換與合一）最一般合一mgu(MostGeneralUnifier)：設是公式集F的一個合一，如果對任一個合一都存在一個置換，使得=則稱是一個最一般的合一?？梢宰C明mgu是唯一的。求mgu算法

基本概念求mgu算法（設公式集為F）：令k=0,Fk=F,k=。是一個空置換。若Fk只含一個表達式，則算法停止，k即為所求的mgu。找出Fk的差異集Dk

。若Dk中存在元素xk和tk

，其中xk是變元，tk是項，且xk不在tk中出現(xiàn)，則置：k+1=k{tk/xk},Fk+1=Fk

{tk/xk

},k=k+1,

然后轉2）算法終止，F(xiàn)的mgu不存在。

基本概念求mgu舉例：

F={P[f(x),y,g(y)],P[f(x),z,g(x)]}

k=0,F0=F,0=,D0={y,z}1=0{y/z}={y/z}F1=F0{y/z

}={P[f(x),y,g(y)],P[f(x),y,g(x)]}k=1,D1={y,x},2=1{y/x}={y/z,y/x}F2=F1{y/z,y/x

}={P[f(y),y,g(y)],P[f(y),y,g(y)]}F2只含一個表達式，則算法停止，2即為所求的mgu。mgu={y/z,y/x}第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理歸結推理命題邏輯謂詞邏輯Skolem標準形、子句集基本概念謂詞邏輯歸結原理合一和置換、控制策略數(shù)理邏輯命題邏輯歸結Herbrand定理第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理基本概念歸結原理由J.A.Robinson由1965年提出。與演繹法完全不同，新的邏輯演算算法。>>>一階邏輯中，至今為止的最有效的半可判定的算法。即，一階邏輯中任意恒真公式，使用歸結原理，總可以在有限步內給以判定。語義網(wǎng)絡、框架表示、產(chǎn)生式規(guī)則等等都是以推理方法為前提的。即，有了規(guī)則已知條件，順藤摸瓜找到結果。而歸結方法是自動推理、自動推導證明用的。（“數(shù)學定理機器證明”）本課程只討論一階謂詞邏輯描述下的歸結推理方法，不涉及高階謂詞邏輯問題。

命題邏輯的歸結法歸結反演推理方法基本思想例：

命題：A1、A2、A3

和B求證：A1∧A2∧A3成立，則B成立，即：A1∧A2∧A3→B反證法：證明A1∧A2∧A3∧B是矛盾式（永假式）

歸結法是以子句集為背景的。

子句的概念子句與子句集文字：不含任何連接詞的命題(謂詞公式)及其否定。子句：任何文字的析取式(謂詞的和)。空子句：不含任何文字的子句?？兆泳涞牟豢蓾M足性：由于空子句不含任何文字，它不能被任何解釋滿足，所以空子句是永假的，不可滿足的。子句集：由子句構成的集合。子句的概念建立子句集合取范式：命題、命題和的與，如：

P∧

（P∨Q）∧（

P∨Q）子句集S：合取范式形式下的子命題（元素）的集合例：命題公式：P∧（P∨Q）∧（P∨Q）子句集S：S={P,P∨Q,P∨Q}

子句的概念謂詞公式F相對應的子句集S的求?。篎→SKOLEM標準形

→消去存在變量

→以“，”取代“∧”，并表示為集合形式。命題邏輯的歸結法歸結過程

將命題寫成合取范式求出子句集對子句集使用歸結推理規(guī)則歸結式作為新子句參加歸結歸結式為空子句□

，S是不可滿足的（矛盾），原命題成立。

（證明完畢）謂詞的歸結：除了有量詞和函數(shù)以外，其余和命題歸結過程一樣。命題邏輯歸結例題（1）例題，證明公式：(P→Q)→(～Q→～P)證明：（1）根據(jù)歸結原理，將待證明公式轉化成待歸結命題公式：

(P→Q)∧～(～Q→～P)（2）分別將公式前項化為合取范式：

P→Q＝～P∨Q

結論求～后的后項化為合取范式： ～(～Q→～P)＝～(Q∨～P)＝～Q∧P

兩項合并后化為合取范式： （～P∨Q）∧～Q∧P

（3）則子句集為：

{～P∨Q，～Q，P}命題邏輯歸結例題（2）子句集為： {～P∨Q，～Q，P}（4）對子句集中的子句進行歸結可得：1.

～P∨Q2.

～Q3.

P4.

Q， （1，3歸結）5.

， （2，4歸結）

由上可得原公式成立。第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理子句形—謂詞公式化為子句集步驟1消去蘊含符號PQP∨Q例：(x){P(x){(y)[P(y)P(f(x,y))]∧

(y)[Q(x,y)P(y)]}}子句形—謂詞公式化為子句集步驟1消去蘊含符號PQP∨Q例：(x){P(x){(y)[P(y)P(f(x,y))]∧

(y)[Q(x,y)P(y)]}}(x){P(x)

∨{(y)[P(y)

∨P(f(x,y))]∧

(y)[Q(x,y)

∨P(y)]}}子句形—謂詞公式化為子句集步驟2減少否定符號的轄域(P)

P(P∧Q)

P∨Q或(P∨Q)

P∧Q(x)P(x)(x)P(x)或(x)P(x)(x)P(x)

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}子句形—謂詞公式化為子句集步驟2減少否定符號的轄域(P)

P(P∧Q)

P∨Q或(P∨Q)

P∧Q(x)P(x)(x)P(x)或(x)P(x)(x)P(x)

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)

[Q(x,y)∨P(y)]}}(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}子句形—謂詞公式化為子句集步驟3變量標準化，即重新命名變元保證每個量詞有其唯一的約束變量。如：(x){P(x)(x)Q(x)}標準化為(x){P(x)(y)Q(y)}

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}

子句形—謂詞公式化為子句集步驟3變量標準化，即重新命名變元保證每個量詞有其唯一的約束變量。如：(x){P(x)(x)Q(x)}標準化為(x){P(x)(y)Q(y)}

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}子句形—謂詞公式化為子句集步驟4消去存在量詞如：(x)P(x,y)用P(A,y)

替換，A為某一常量。如：(y){(x)P(x,y)}引入Skolem函數(shù)g(y)，用(y)

P(g(y),y)

替換例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}

子句形—謂詞公式化為子句集步驟4消去存在量詞如：(x)P(x,y)用P(A,y)

替換，A為某一常量。如：(y){(x)P(x,y)}引入Skolem函數(shù)g(y)，用(y)

P(g(y),y)

替換例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}子句形—謂詞公式化為子句集步驟4消去存在量詞量詞消去原則： 消去存在量詞“”，略去全稱量詞“”。

注意：左邊有全稱量詞的存在量詞，消去時該變量改寫成為全稱量詞的函數(shù)；如沒有，改寫成為常量。

子句形—謂詞公式化為子句集步驟5化為前束形如把所有全稱量詞移到公式的左邊，并使得每個量詞的轄域包含這個量詞后面公式的整個部分，所得公式稱為前束形。例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}

子句形—謂詞公式化為子句集步驟5化為前束形如把所有全稱量詞移到公式的左邊，并使得每個量詞的轄域包含這個量詞后面公式的整個部分，所得公式稱為前束形。例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}

(x)(y){P(x)∨{

[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標準形前束范式：把所有的量詞都提到前面去，然后消掉所有量詞。

定義：說公式A是一個前束范式，如果A中的一切量詞都位于該公式的最左邊（不含否定詞），且這些量詞的轄域都延伸到公式的末端。SKOLEM標準形==（全稱量詞串）{母式}母式：子句的合取式子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標準形反復利用分配率，把任一個母式化為合取范式。A∨(B∧

C)

(A∨B)

∧(A∨C)

例：(x)(y){P(x)∨{

[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標準形反復利用分配率，把任一個母式化為合取范式。A∨(B∧

C)

(A∨B)

∧(A∨C)

例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}(x)(y){{P(x)

∨[P(y)∨P(f(x,y))]}∧{P(x)

∨[

Q(x,g(x))∧

P(g(x))]}}子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標準形反復利用分配率，把任一個母式化為合取范式。A∨(B∧

C)

(A∨B)

∧(A∨C)

例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧{P(x)

∨[

Q(x,g(x))

∧

P(g(x))]}}(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧[P(x)

∨Q(x,g(x))]∧[P(x)

∨

P(g(x))]}子句形—謂詞公式化為子句集步驟7消去全稱量詞例：

(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))]}[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))]子句形—謂詞公式化為子句集步驟8對變元更名使得一個變元符號不出現(xiàn)在一個以上的子句中。例：

[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))][P(x1)∨P(y)∨P(f(x1,y))]∧[P(x2)∨Q(x2,g(x2))]∧[P(x3)∨

P(g(x3))]子句形—謂詞公式化為子句集步驟9消去合取符號用子句集代替合取式，即為所求的子句集。例：

[P(x1)∨P(y)∨P(f(x1,y))]∧[P(x2)∨Q(x2,g(x2))]∧[P(x3)∨

P(g(x3))]{P(x1)∨P(y)∨P(f(x1,y))，P(x2)∨Q(x2,g(x2))，P(x3)∨

P(g(x3))}子句形定理： 謂詞邏輯的任意公式都可以化為與之等價的前束范式，但其前束范式不唯一。SKOLEM標準形定義： 消去量詞后的謂詞公式。注意：謂詞公式F的SKOLEM標準形同F(xiàn)并不等值。子句形

F是不可滿足的S是不可滿足的F與S不等價，但在不可滿足的意義下是一致的。

定理：

若F是給定的公式，而S是相應的子句集，則F是不可滿足的S是不可滿足的。

注意：F真不一定S真，而S真必有F真。 即：S

F子句形把F的不可滿足判斷S的不可滿足引用Herbrand定理，研究S的不可滿足性。引用Herbrand定理，以說明歸結原理的意義及一個原理形成的根基與背景。采用歸結反演方法判定S的不可滿足性。

第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理歸結原理基本思想通過歸結方法不斷擴充待判定的子句集，并設法使其包含進指示矛盾的空子句。空子句是不可滿足（即永假）的子句，既然子句集中子句間隱含著合取關系，空子句的出現(xiàn)實際上判定了子句集的不可滿足。定義：若P是原子謂詞公式，則稱P與P為互補文字（互補對）。命題邏輯的歸結法命題邏輯的歸結

設有子句C1,C2，如果C1中的文字L1與C2中的文字L2互補，則消除互補對，余下部分析取求得新子句→得到歸結式C12

。例：C1

C2

C12

PP∨Q

Q假言推理

P∨QP∨Q

Q∨Q=Q合并

P∨QP∨

Q

Q∨

Q重言式

P∨QP∨

Q

P∨PPP

□或

NIL空子句

P∨QQ∨R

P∨R

三段論命題邏輯的歸結法歸結式性質定理：兩個子句C1和C2的歸結式C12是C1和C2的邏輯推論，即C1∧C2C12（在任一個使子句C1和C2為真的解釋I下，必有歸結式C12為真）推論1：子句集S中子句C1和C2的歸結式為C12，若用C12

代替C1和C2后得到新子句集S1，則S1不可滿足性

S的不可滿足性推論2：子句集S中子句C1和C2的歸結式為C12，若把C12

加入S中得到新子句集S2，則S2不可滿足性

S的不可滿足性謂詞邏輯的歸結法謂詞邏輯的歸結（含有變量子句的歸結）設有兩個沒有相同變元的子句C1,C2，L1是C1中的文字與L2是C2中的文字，若是L1和L2的mgu，則稱C12=(C1

-{L1

})∨

(C2

-{L2

})為子句C1,C2的二元歸結式。謂詞邏輯的歸結法例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(z)

取L1為P[x,f(A)]，L2為P[z,f(A)]

則={x/z}得C12=P[x,f(y)]∨Q(y)∨

Q(x)例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(z)

取L1為Q(y)，L2為Q(z)

則={y/z}得C12=P[x,f(A)]∨P[x,f(y)]∨

P[y,f(A)]

可進一步歸結得到

P[x,f(x)]

謂詞邏輯的歸結法例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(x)

取L1為P[x,f(A)]，L2為P[z,f(A)]

則={x/z}得C12=P[x,f(y)]∨Q(y)∨Q(x)

修改C2變元名P[z,f(A)]∨Q(x1)

則={x/z}得C12=P[x,f(y)]∨Q(y)∨

Q(x1)歸結反演歸結原理正確性的根本在于，找到矛盾可以肯定不真。方法：和命題邏輯一樣。但由于有函數(shù)，所以要考慮合一和置換。

歸結反演置換和合一的注意事項：謂詞的一致性，P()與Q()，

不可以常量的一致性，P(a,…)與P(b,….)，

不可以

變量，P(a,….)與P(x,…)，

可以變量與函數(shù)，P(a,x,….)與P(x,f(x),…)，不可以；但P(a,z,…)與P(x,f(y),…)，可以不能同時消去兩個互補對，P∨Q與P∨Q的空，不可以先進行內部簡化（置換、合并）

歸結反演—在定理證明中的應用歸結反演的基本思想

目標公式被否定并化為子句集，添加到命題公式集中，用歸結反演應用于聯(lián)合集，并力圖推導出一個空子句（□或NIL）表示產(chǎn)生一個矛盾，定理得證。歸結反演—在定理證明中的應用歸結反演的過程（證明F→Q）寫出謂詞關系公式F（前提）和Q（目標、結論）否定目標Q加入公式集F,寫出謂詞表達式{F,Q}求SKOLEM標準形化為子句集S對S中可歸結的子句做歸結歸結式仍放入S中，反復歸結過程得到空子句□(NIL)

，得證歸結反演—在定理證明中的應用證明：每個儲蓄錢的人都獲得利息，若沒有利息就沒有人去儲蓄錢。令：S(x,y)表示x儲蓄yM(x)表示x是錢

I(x)表示x是利息E(x,y)表示x獲得y則前提為

(x)[(y)(

S(x,y)∧M(y))(y)(I(y)∧E(x,y))]

結論為

(x)I(x)(x)(y)(

S(x,y)

M(y))

歸結反演—在定理證明中的應用

F:

(x)[(y)(

A(x,y)∧B(y))(y)(C(y)∧D(x,y))]

G:

(x)C(x)(x)(y)(

A(x,y)

B(y))

F化為子句得

A(x,y)∨

B(y)∨C(f(x))………….(1)

A(x,y)∨

B(y)∨D(x,f(x))………….(2)G化為子句得

C(z)……….(3)A(a,b)………..(4)B(b)……….(5)歸結反演—在定理證明中的應用A(x,y)∨B(y)∨D(x,f(x))A(x,y)∨B(y)∨C(f(x))C(z)A(a,b)B(b)(1)(2)(3)(4)(5)NIL(8)B(b)∨C(f(a))(6){a/x,b/y}B(b)(7){f(a)/z}歸結反演—在定理證明中的應用歸結反演基本算法：給定公式F對應的子句集S，求證目標公式G成立。

①CLAUSES←S∪{G}②UntilNIL是CLAUSES的成員，do：

③begin④在子句集CLAUSES中選擇二個不同的可歸結的子句Ci,Cj⑤計算Ci,Cj的歸結式Cij⑥CLAUSES←將Cij加入到CLAUSES中

⑦end說明：可歸結子句的選擇次序可以是任意的。歸結反演—在定理證明中的應用

證明：梯形的對角線與上下底構成的內錯角相等。引入謂詞：T(x,y,u,v)表示xy為上底，uv為下底的梯形。

P(x,y,u,v)表示xy//uv。

E(x,y,z,u,v,w)表示∠xyz=∠uvw。xvuy梯形上下底平行平行內錯角相等歸結反演—在定理證明中的應用

問題描述：A1:(x)(y)(u)(v)((T(x,y,u,v)P(x,y,u,v))

//上下底平行A2:(x)(y)(u)(v)((P(x,y,u,v)E(x,y,v,u,v,y))

//平行內錯角相等A3:T(a,b,c,d)

G:E(a,b,d,c,d,b)

化為子句：

A1:

T(x,y,u,v)∨P(x,y,u,v)A2:P(x,y,u,v)∨E(x,y,v,u,v,y)A3:T(a,b,c,d)

G:E(a,b,d,c,d,b)acdb歸結反演—在定理證明中的應用T(x,y,u,v)∨P(x,y,u,v)P(x,y,u,v)∨E(x,y,v,u,v,y)T(a,b,c,d)E(a,b,d,c,d,b)(1)(2)(3)(4)(6)(5)P(a,b,c,d)P(a,b,c,d)NIL歸結反演—在定理證明中的應用證明如下公式G是否為F的邏輯結論

答案:

是歸結反演—求解問題的答案基于歸結法的問答系統(tǒng)問答系統(tǒng)要解決的問題形式：有二種類型：直接問答：求證當x=A時，G(A)成立。即：真假證明間接問答：求證當x=？時，G(x)成立。即：求值證明前面的證明方法都屬于直接問答。間接問答方法需要采用構造方法。歸結反演—求解問題的答案例題：如果Peter去那兒，則John就去那兒。如果Peter在學校。問題：

John去哪兒？解：用謂詞公式表達所有前提以及結論。

①②結論：歸結反演—求解問題的答案子句集：上面證明了：在給定前提下結論成立。

但是沒有給出：John在哪兒。解決問題的辦法是：歸結反演—求解問題的答案解決問題的辦法：①由目標公式的否定與目標公式的析取構成重言式(G∨G)，將其加入到公式集中，取代原來公式集中目標公式的否定式。②依據(jù)反演樹的構造方法進行歸結，直到得到某個子句為止。③以該子句作為對問題的回答。歸結反演—求解問題的答案上例中，用取代答案是：John在學校。歸結反演—求解問題的答案求解的過程寫出謂詞關系公式F（已知前提）求SKOLEM標準形，化為子句集S寫出待求解問題的謂詞公式，然后把它否定并與形式謂詞ANSWER構成析取式（變元一致）把該析取式化為子句集并入到S中，得到子句集S’對S’中可歸結的子句做歸結歸結式仍放入S中，反復歸結過程得到歸結式ANSWER，則答案就在ANSWER中。問題得到解。歸結反演—求解問題的答案上例中，用取代答案是：John在學校。歸結反演—求解問題的答案求猴子吃香蕉問題的答案：A1(x)(y)(z)(s)(P(x,y,z,s)P(z,y,z,Walk(x,z,s)))A2(x)(y)(s)(P(x,y,x,s)P(y,y,y,Carry(x,y,s)))A3(s)(P(b,b,b,s)R(Climb(s)))A4P(a,b,c,s0)A5R(s)∨ANS(s)歸結反演—求解問題的答案化為子句：A1P(x,y,z,s)∨P(z,y,z,Walk(x,z,s))………….(1)A2P(x,y,x,s)∨P(y,y,y,Carry(x,y,s))………….(2)A3P(b,b,b,s)∨R(Climb(s))…………..(3)A4P(a,b,c,s0)…………..(4)A5R(s)∨ANS(s)…………..(5)歸結反演—求解問題的答案歸結P(x1,y,z,s3)∨P(z,y,z,Walk(x1,z,s3))(1)P(x,y,x,s2)∨P(y,y,y,Carry(x,y,s2))(2)P(a,b,c,s0)(4)R(s1)∨ANS(s1)(5)P(b,b,b,s)∨R(Climb(s))(3)P(b,b,b,s)∨ANS(Climb(s))(6)P(x,b,x,s2)∨ANS(Climb(Carry(x,b,s2)))(7)P(x1,b,z,s3)∨ANS(Climb(Carry(z,b,Walk(x1,z,s3))))(8)ANS(Climb(Carry(c,b,Walk(a,c,s0))))(9){Climb(s)/s1}{b/y,Carry(x,b,s2)/s}{z/x,b/y,Walk(x1,z,s3)/s2}{a/x1,c/z,s0/s3}歸結反演歸結法的實質：歸結法是僅有一條推理規(guī)則的推理方法。歸結的過程是一個語義樹倒塌的過程。歸結法的問題子句中有等號或不等號時，完備性不成立。※Herbrand定理的不實用性引出了可實用的歸結法。第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理歸結策略例設已知1）能閱讀的人是識字的。2）海豚不識字。3）有些海豚是聰明的。證明：有些很聰明的人并不能閱讀。引入謂詞L(x)表示識字、R(x)能閱讀、D(x)海豚、I(x)有智力

1)(x)(R(x)L(x))2)(x)(D(x)

L(x))3)(x)(D(x)∧I(x))G:(x)(I(x)∧

R(x))

對應子句

1)R(x)∨L(x)2)D(y)∨

L(y)3a)D(A)3b)I(A)4)I(z)∨R(z)歸結策略---寬度優(yōu)先策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)第二級歸結第三級歸結第一級歸結歸結策略---寬度優(yōu)先策略

寬度優(yōu)先：⑴首先歸結出基本集S0∪{~G}所有可能的歸結式（第一級歸結）。例：⑵再同理歸結出第二級歸結式。例：⑶依次類推，直到出現(xiàn)NIL子句。優(yōu)點：具有完備性不足：效率低，代價大R(A)L(A)NIL歸結策略實用上，歸結反演系統(tǒng)面臨著大子句集而引起的演繹效率問題。解決問題的關鍵在于選擇有利于導致快速產(chǎn)生空子句的子句進行歸結。若盲目地隨機選擇子句對進行歸結，不僅要耗時，而且還會歸結出許多無用的歸結式而過分擴張了子句集，從而浪費了時空，并降低了效率。研究歸結策略成為促進歸結演繹技術實用化的重點。歸結策略要解決的問題：歸結方法的知識爆炸?？刂撇呗缘哪康臍w結點盡量少控制策略的原則給出控制策略，以使僅對選擇合適的子句間方可做歸結。避免多余的、不必要的歸結式出現(xiàn)。或者說，少做些歸結仍能導出空子句?？刂撇呗缘姆诸悇h除策略限制策略歸結策略控制策略的方法刪除策略支持集策略 完備輸入策略不完備單文字子句策略不完備祖先過濾策略 完備限制策略歸結策略刪除策略純文字刪除法：找不到與之互補的文字為純文字。歸結時把它所在的子句從子句集中刪去。重言式刪除法：一個子句中同時包含互補文字的子句為重言式，刪除它不影響其所在子句集的不可滿足性。包孕刪除法：設有兩個子句C1,C2，若存在一個代換，使得C1

C2則稱C1,包孕于C2的二元歸結式。把子句集中包孕的子句刪去，不影響子句集的不可滿足性。歸結策略支持集策略：每次歸結，親本子句中至少應有一個是由目標公式的否定所得到的子句，或者是它們的后裔。

支持集策略是完備的它相當于帶有約束條件的寬度優(yōu)先策略歸結子句集的增長速度較寬度優(yōu)先策略慢歸結策略---寬度優(yōu)先策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)G歸結策略---支持集策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)GD(A)NIL歸結策略---支持集策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)GD(A)NIL歸結策略輸入策略：參加歸結的兩個子句中必須至少有一個是初始子句集（基本集）中的子句。

線性輸入策略是不完備的。有些存在反演的系統(tǒng)不一定存在線性輸入反演。說明：因為每個歸結式的父節(jié)點中至少有一個是基本集成員，所以NIL的父節(jié)點也必有一個父節(jié)點來自基本集。歸結策略---寬度優(yōu)先策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)歸結策略---輸入策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)NIL歸結策略---輸入策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)NIL>>>>歸結策略單文字子句(單元)策略：要求參加歸結的兩個子句中必須至少有一個是單文字（子句中只包含一個文字）子句。

單文字子句策略是不完備的。所得到的歸結式中的文字比與該單元子句進行歸結的另一個子句中的文字少歸結策略---寬度優(yōu)先策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)歸結策略---單文字子句策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)NILNIL歸結策略---單文字子句策略的反演圖R(x)∨L(x)D(y)∨

L(y)D(A)I(A)I(z)∨R(z)R(A)I(z)∨L(z)R(y)∨

D(y)L(A)L(A)D(A)I(z)∨

D(z)R(A)I(A)L(A)NILNILI(A)NILNIL歸結策略祖先過濾策略：對兩個子句C1,C2進行歸結時，要求滿足以下2個條件中的任一個。

C1,C2中至少有一個是初始子句集中的子句。（輸入策略）否則，C1,C2中一個應是另一個的祖先。輸入策略是該策略的一種特殊情況。該策略是完備的。

歸結策略---祖先過濾策略的反演圖P(x)∨Q(x)Q(y)∨P(y)Q(z)∨

P(z)P(x)P(x)Q(x)NILQ(t)∨P(t)歸結策略---線性策略線性歸結策略首先從子句集中選取一個稱作頂子句的子句C0開始作歸結。歸結過程中所得到的歸結式Ci立即同另一子句Bi進行歸結得歸結式Ci+1。而Bi屬于S或是已出現(xiàn)的歸結式Cj(j<i)。即，如下圖所示歸結得到的新子句立即參加歸結。線性歸結是完備的，同樣，所有可歸結的謂詞公式都可以采用線性歸結策略達到加快歸結速度的目的。如果能搞找到一個較好的頂子句，可以式歸結順利進行。否則也可能事與愿違。歸結策略---線性策略C0C1C2C3C4C5空線性歸結策略示意圖歸結策略---策略的組合策略的組合：針對某些具體問題，綜合運用上述若干策略。如：支持集與輸入組合；支持集與祖先過濾組合等。第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理第三章謂詞邏輯與歸結原理把F的不可滿足判斷S的不可滿足引用Herbrand定理，研究S的不可滿足性。引用Herbrand定理，以說明歸結原理的意義及一個原理形成的根基與背景

第三章謂詞邏輯與歸結原理基本概念命題邏輯的歸結法子句形歸結原理歸結過程的策略控制Herbrand定理Herbrand定理名詞:

公式F永真:對于F的所有解釋,F都為真.

公式F永假:沒有一個解釋使F為真.問題：

要判定一個子句集是不可滿足的,就是要判定該子句集中的每一個子句都是不可滿足的;要判定一個子句是不可滿足的,則需要判定該子句對任何非空個體域的任意解釋都是不可滿足的.可見,判定子句集的不可滿足性是一件非常困難的工作.

Herbrand定理問題： 一階邏輯公式的永真性（永假性）的判定是否能在有限步內完成？Herbrand定理1936年圖靈(Turing)和邱吉(Church)互相獨立地證明了：

“沒