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

q析取式：

p或q，記做p∨

q蘊(yùn)含式：如果p則q，記做p→

q等價(jià)式：p當(dāng)且僅當(dāng)q，記做p<=>

q

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

∨p

；

p∧q<=>q∧

p

結(jié)合率：(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)

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

(p∨q)

<=>～

p∧

～

q

；

～

(p∧

q)

<=>～

p∨

～

q

吸收率:p∨(p∧

q)<=>p

；

pΛ(p∨q)<=>p

同一律:p∨0

<=>p

；

p∧1

<=>p

蘊(yùn)含等值式:p→

q

<=>～

p∨q

假言易位式:p→

q

<=>～p→～

q

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

簡(jiǎn)單陳述句描述事實(shí)、事物的狀態(tài)、關(guān)系等性質(zhì)。例如：1．

1+1=22．

雪是黑色的。3．

北京是中國(guó)的首都。4．

到冥王星去渡假。

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

快點(diǎn)走吧！

2．

到那去？

3．

x+y>10

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

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

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

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

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

∧(r∨t)→

q。

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

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

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

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

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

。聯(lián)結(jié)詞：為了表現(xiàn)更復(fù)雜的內(nèi)容，聯(lián)結(jié)各簡(jiǎn)單謂詞公式構(gòu)成復(fù)合謂詞公式的詞。有∨

謂詞邏輯基礎(chǔ)合式公式：?jiǎn)蝹€(gè)謂詞是合式公式，成為原子謂詞公式。若A是合式公式，則A也是合式公式。若A，B是合式公式，則AB,A∨B,AB,AB也是合式公式。若A是合式公式，x是任一個(gè)體變?cè)瑒t(x)A和(x)A也是合式公式。 謂詞邏輯基礎(chǔ)謂詞公式的等價(jià)式

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

P∨

Q,(P∨Q)

P

Q

雙重否定律

QQ連接詞化歸律PQ

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

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

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

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

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

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

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

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

Commit(x)→Punished(x)，x犯了罪就一定要受到懲罰。 而，{[Human(x)→Lawed(x)]→[commit(x)→Punished(x)]}， 意為如果由于某個(gè)x是人而受法律管制，則這個(gè)人犯了罪就一定要受到懲罰。一階謂詞邏輯知識(shí)表示方法例：兔子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))一階謂詞邏輯知識(shí)表示方法謂詞邏輯表示法在實(shí)際人工智能系統(tǒng)上得到應(yīng)用。機(jī)器人行動(dòng)（如圖示）1.引入謂詞

Table(x):x是桌子

Empty(y):y手中為空

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

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

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

目標(biāo)狀態(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)一階謂詞邏輯知識(shí)表示方法機(jī)器人行動(dòng)2.引入算子（狀態(tài)轉(zhuǎn)移函數(shù)）

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

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

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

一階謂詞邏輯知識(shí)表示方法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)一階謂詞邏輯知識(shí)表示方法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)一階謂詞邏輯知識(shí)表示方法

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

P(x,y,z,s):猴子在x處，香蕉在y處，梯子在z處，相應(yīng)狀態(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.問題描述……一階謂詞邏輯知識(shí)表示方法

“猴子吃香蕉”問題的描述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í)表示方法謂詞邏輯法是應(yīng)用最廣的方法之一，其原因是：謂詞邏輯與數(shù)據(jù)庫，特別是關(guān)系數(shù)據(jù)庫就有密切的關(guān)系。在關(guān)系數(shù)據(jù)庫中，邏輯代數(shù)表達(dá)式是謂詞表達(dá)式之一。因此，如果采用謂詞邏輯作為系統(tǒng)的理論背景，則可將數(shù)據(jù)庫系統(tǒng)擴(kuò)展改造成知識(shí)庫。

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

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

基本概念模式匹配（置換與合一）置換：有序?qū)Φ募蟂={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

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

和={u1/y1,u2/y2,…,un/yn}是兩個(gè)置換。則兩個(gè)置換的復(fù)合也是一個(gè)置換。={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}性質(zhì)：滿足結(jié)合律，而不滿足交換律（1）2=（12），而一般1221

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

F1=F2=…=Fn

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

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

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

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

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

。若Dk中存在元素xk和tk

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

{tk/xk

},k=k+1,

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

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

命題：A1、A2、A3

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

歸結(jié)法是以子句集為背景的。

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

P∧

（P∨Q）∧（

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

子句的概念謂詞公式F相對(duì)應(yīng)的子句集S的求?。篎→SKOLEM標(biāo)準(zhǔn)形

→消去存在變量

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

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

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

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

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

P→Q＝～P∨Q

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

兩項(xiàng)合并后化為合取范式： （～P∨Q）∧～Q∧P

（3）則子句集為：

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

～P∨Q2.

～Q3.

P4.

Q， （1，3歸結(jié)）5.

， （2，4歸結(jié)）

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

(y)[Q(x,y)P(y)]}}子句形—謂詞公式化為子句集步驟1消去蘊(yùn)含符號(hào)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減少否定符號(hào)的轄域(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減少否定符號(hào)的轄域(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變量標(biāo)準(zhǔn)化，即重新命名變?cè)ＷC每個(gè)量詞有其唯一的約束變量。如：(x){P(x)(x)Q(x)}標(biāo)準(zhǔn)化為(x){P(x)(y)Q(y)}

例：

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

(y)[

Q(x,y)∧

P(y)]}}

子句形—謂詞公式化為子句集步驟3變量標(biāo)準(zhǔn)化，即重新命名變?cè)ＷC每個(gè)量詞有其唯一的約束變量。如：(x){P(x)(x)Q(x)}標(biāo)準(zhǔn)化為(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í)該變量改寫成為全稱量詞的函數(shù)；如沒有，改寫成為常量。

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

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

Q(x,g(x))∧

P(g(x))]}}

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

(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標(biāo)準(zhǔn)形前束范式：把所有的量詞都提到前面去，然后消掉所有量詞。

定義：說公式A是一個(gè)前束范式，如果A中的一切量詞都位于該公式的最左邊（不含否定詞），且這些量詞的轄域都延伸到公式的末端。SKOLEM標(biāo)準(zhǔn)形==（全稱量詞串）{母式}母式：子句的合取式子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標(biāo)準(zhǔn)形反復(fù)利用分配率，把任一個(gè)母式化為合取范式。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標(biāo)準(zhǔn)形反復(fù)利用分配率，把任一個(gè)母式化為合取范式。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標(biāo)準(zhǔn)形反復(fù)利用分配率，把任一個(gè)母式化為合取范式。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對(duì)變?cè)沟靡粋€(gè)變?cè)?hào)不出現(xiàn)在一個(gè)以上的子句中。例：

[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消去合取符號(hào)用子句集代替合取式，即為所求的子句集。例：

[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))}子句形定理： 謂詞邏輯的任意公式都可以化為與之等價(jià)的前束范式，但其前束范式不唯一。SKOLEM標(biāo)準(zhǔn)形定義： 消去量詞后的謂詞公式。注意：謂詞公式F的SKOLEM標(biāo)準(zhǔn)形同F(xiàn)并不等值。子句形

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

定理：

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

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

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

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

設(shè)有子句C1,C2，如果C1中的文字L1與C2中的文字L2互補(bǔ)，則消除互補(bǔ)對(duì)，余下部分析取求得新子句→得到歸結(jié)式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

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

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

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

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

S的不可滿足性謂詞邏輯的歸結(jié)法謂詞邏輯的歸結(jié)（含有變量子句的歸結(jié)）設(shè)有兩個(gè)沒有相同變?cè)淖泳銫1,C2，L1是C1中的文字與L2是C2中的文字，若是L1和L2的mgu，則稱C12=(C1

-{L1

})∨

(C2

-{L2

})為子句C1,C2的二元?dú)w結(jié)式。謂詞邏輯的歸結(jié)法例：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)]

可進(jìn)一步歸結(jié)得到

P[x,f(x)]

謂詞邏輯的歸結(jié)法例：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變?cè)鸓[z,f(A)]∨Q(x1)

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

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

歸結(jié)反演置換和合一的注意事項(xiàng)：謂詞的一致性，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),…)，可以不能同時(shí)消去兩個(gè)互補(bǔ)對(duì)，P∨Q與P∨Q的空，不可以先進(jìn)行內(nèi)部簡(jiǎn)化（置換、合并）

歸結(jié)反演—在定理證明中的應(yīng)用歸結(jié)反演的基本思想

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

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

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

(x)[(y)(

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

結(jié)論為

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

S(x,y)

M(y))

歸結(jié)反演—在定理證明中的應(yīng)用

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)歸結(jié)反演—在定理證明中的應(yīng)用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}歸結(jié)反演—在定理證明中的應(yīng)用歸結(jié)反演基本算法：給定公式F對(duì)應(yīng)的子句集S，求證目標(biāo)公式G成立。

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

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

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

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

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

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

問題描述：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))

//平行內(nèi)錯(cuò)角相等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歸結(jié)反演—在定理證明中的應(yīng)用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歸結(jié)反演—在定理證明中的應(yīng)用證明如下公式G是否為F的邏輯結(jié)論

答案:

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

John去哪兒？解：用謂詞公式表達(dá)所有前提以及結(jié)論。

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

但是沒有給出：John在哪兒。解決問題的辦法是：歸結(jié)反演—求解問題的答案解決問題的辦法：①由目標(biāo)公式的否定與目標(biāo)公式的析取構(gòu)成重言式(G∨G)，將其加入到公式集中，取代原來公式集中目標(biāo)公式的否定式。②依據(jù)反演樹的構(gòu)造方法進(jìn)行歸結(jié)，直到得到某個(gè)子句為止。③以該子句作為對(duì)問題的回答。歸結(jié)反演—求解問題的答案上例中，用取代答案是：John在學(xué)校。歸結(jié)反演—求解問題的答案求解的過程寫出謂詞關(guān)系公式F（已知前提）求SKOLEM標(biāo)準(zhǔn)形，化為子句集S寫出待求解問題的謂詞公式，然后把它否定并與形式謂詞ANSWER構(gòu)成析取式（變?cè)恢拢┌言撐鋈∈交癁樽泳浼⑷氲絊中，得到子句集S’對(duì)S’中可歸結(jié)的子句做歸結(jié)歸結(jié)式仍放入S中，反復(fù)歸結(jié)過程得到歸結(jié)式ANSWER，則答案就在ANSWER中。問題得到解。歸結(jié)反演—求解問題的答案上例中，用取代答案是：John在學(xué)校。歸結(jié)反演—求解問題的答案求猴子吃香蕉問題的答案：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)歸結(jié)反演—求解問題的答案化為子句：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)歸結(jié)反演—求解問題的答案歸結(jié)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}歸結(jié)反演歸結(jié)法的實(shí)質(zhì)：歸結(jié)法是僅有一條推理規(guī)則的推理方法。歸結(jié)的過程是一個(gè)語義樹倒塌的過程。歸結(jié)法的問題子句中有等號(hào)或不等號(hào)時(shí)，完備性不成立?！鵋erbrand定理的不實(shí)用性引出了可實(shí)用的歸結(jié)法。第三章謂詞邏輯與歸結(jié)原理基本概念命題邏輯的歸結(jié)法子句形歸結(jié)原理歸結(jié)過程的策略控制Herbrand定理第三章謂詞邏輯與歸結(jié)原理基本概念命題邏輯的歸結(jié)法子句形歸結(jié)原理歸結(jié)過程的策略控制Herbrand定理歸結(jié)策略例設(shè)已知1）能閱讀的人是識(shí)字的。2）海豚不識(shí)字。3）有些海豚是聰明的。證明：有些很聰明的人并不能閱讀。引入謂詞L(x)表示識(shí)字、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))

對(duì)應(yīng)子句

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

L(y)3a)D(A)3b)I(A)4)I(z)∨R(z)歸結(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)第二級(jí)歸結(jié)第三級(jí)歸結(jié)第一級(jí)歸結(jié)歸結(jié)策略---寬度優(yōu)先策略

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

C2則稱C1,包孕于C2的二元?dú)w結(jié)式。把子句集中包孕的子句刪去，不影響子句集的不可滿足性。歸結(jié)策略支持集策略：每次歸結(jié)，親本子句中至少應(yīng)有一個(gè)是由目標(biāo)公式的否定所得到的子句，或者是它們的后裔。

支持集策略是完備的它相當(dāng)于帶有約束條件的寬度優(yōu)先策略歸結(jié)子句集的增長(zhǎng)速度較寬度優(yōu)先策略慢歸結(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)G歸結(jié)策略---支持集策略的反演圖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歸結(jié)策略---支持集策略的反演圖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歸結(jié)策略輸入策略：參加歸結(jié)的兩個(gè)子句中必須至少有一個(gè)是初始子句集（基本集）中的子句。

線性輸入策略是不完備的。有些存在反演的系統(tǒng)不一定存在線性輸入反演。說明：因?yàn)槊總€(gè)歸結(jié)式的父節(jié)點(diǎn)中至少有一個(gè)是基本集成員，所以NIL的父節(jié)點(diǎn)也必有一個(gè)父節(jié)點(diǎn)來自基本集。歸結(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)歸結(jié)策略---輸入策略的反演圖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歸結(jié)策略---輸入策略的反演圖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>>>>歸結(jié)策略單文字子句(單元)策略：要求參加歸結(jié)的兩個(gè)子句中必須至少有一個(gè)是單文字（子句中只包含一個(gè)文字）子句。

單文字子句策略是不完備的。所得到的歸結(jié)式中的文字比與該單元子句進(jìn)行歸結(jié)的另一個(gè)子句中的文字少歸結(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)歸結(jié)策略---單文字子句策略的反演圖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歸結(jié)策略---單文字子句策略的反演圖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歸結(jié)策略祖先過濾策略：對(duì)兩個(gè)子句C1,C2進(jìn)行歸結(jié)時(shí)，要求滿足以下2個(gè)條件中的任一個(gè)。

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

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

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

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

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

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

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

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

“沒