歸結(jié)推理方法

歸結(jié)推理方法第一頁(yè)，共一百四十八頁(yè)，2022年，8月28日2歸結(jié)推理命題邏輯謂詞邏輯Skolem標(biāo)準(zhǔn)形、子句集基本概念謂詞邏輯歸結(jié)原理合一和置換、控制策略數(shù)理邏輯命題邏輯歸結(jié)Herbrand定理第二頁(yè)，共一百四十八頁(yè)，2022年，8月28日3第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制第三頁(yè)，共一百四十八頁(yè)，2022年，8月28日4概述歸結(jié)原理由由1965年提出。與演繹法(deductiveinference)完全不同,新的邏輯演算(inductiveinference)算法。一階邏輯中,至今為止的最有效的半可判定的算法。即,一階邏輯中任意恒真公式,使用歸結(jié)原理,總可以在有限步內(nèi)給以判定。語(yǔ)義網(wǎng)絡(luò)、框架表示、產(chǎn)生式規(guī)則等等都是以推理方法為前提的。即,有了規(guī)則已知條件,順藤摸瓜找到結(jié)果。而歸結(jié)方法是自動(dòng)推理、自動(dòng)推導(dǎo)證明用的。(“數(shù)學(xué)定理機(jī)器證明”)本課程只討論一階謂詞邏輯描述下的歸結(jié)推理方法,不涉及高階謂詞邏輯問(wèn)題。第四頁(yè)，共一百四十八頁(yè)，2022年，8月28日5第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第五頁(yè)，共一百四十八頁(yè)，2022年，8月28日6第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第六頁(yè)，共一百四十八頁(yè)，2022年，8月28日7命題例命題：能判斷真假(不是既真又假)的陳述句。 簡(jiǎn)單陳述句描述事實(shí)、事物的狀態(tài)、關(guān)系等性質(zhì)。例如：1.

1+1=22.

雪是黑色的。

3.

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

4.

我到冥王星去渡假。第七頁(yè)，共一百四十八頁(yè)，2022年，8月28日8命題例判斷一個(gè)句子是否是命題,有先要看它是否是陳述句,而后看它的真值是否唯一。以上的例子都是陳述句,第4句的真值現(xiàn)在是假,隨著人類科學(xué)的發(fā)展,有可能變成真,但不管怎樣,真值是唯一的。因此,以上4個(gè)例子都是命題。而例如：1.

快點(diǎn)走吧！

2.

到那去？

3.

x+y>10

等等句子,都不是命題。第八頁(yè)，共一百四十八頁(yè)，2022年，8月28日9命題邏輯的歸結(jié)法命題邏輯基礎(chǔ)：定義：合取式：p與q,記做pq析取式：p或q,記做pq蘊(yùn)含式：如果p則q,記做p→q等價(jià)式：p當(dāng)且僅當(dāng)q,記做pq

。。。。。。第九頁(yè)，共一百四十八頁(yè)，2022年，8月28日10命題表示公式(1)將陳述句轉(zhuǎn)化成命題公式。如：設(shè)“下雨”為p,“騎車上班”為q,1.“只要不下雨,我騎自行車上班”。p是q的充分條件,

因而,可得命題公式：p→q2.“只有不下雨,我才騎自行車上班”。

p是q的必要條件,

因而,可得命題公式：q→p第十頁(yè)，共一百四十八頁(yè)，2022年，8月28日11命題表示公式(2)例如：1.

“如果我進(jìn)城我就去看你,除非我很累?！痹O(shè)：p,我進(jìn)城,q,去看你,r,我很累。 則有命題公式：

r→(p→q)。2.“應(yīng)屆高中生,得過(guò)數(shù)學(xué)或物理競(jìng)賽的一等獎(jiǎng),保送上北京大學(xué)。”設(shè)：p,應(yīng)屆高中生,q,保送上北京大學(xué)上學(xué),r,是得過(guò)數(shù)學(xué)一等獎(jiǎng)。t,是得過(guò)物理一等獎(jiǎng)。則有命題公式公式：p∧(r∨t)→q。第十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日12命題邏輯基礎(chǔ)定義：若A無(wú)成假賦值,則稱A為重言式或永真式；若A無(wú)成真賦值,則稱A為矛盾式或永假式；若A至少有一個(gè)成真賦值,則稱A為可滿足的；析取范式：僅由有限個(gè)簡(jiǎn)單合取式組成的析取式。合取范式：僅由有限個(gè)簡(jiǎn)單析取式組成的合取式。第十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日13命題邏輯基礎(chǔ)基本等值式24個(gè)(1)交換律：pqq

p

；

pqq

p

結(jié)合律：(pq)rp(qr); (p

q)rp(qr)分配律：p(qr)(p

q)(p

r)；

p(qr)(pq)(p

r)第十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日14命題邏輯基礎(chǔ)基本等值式(1)摩根律:(pq)

pq；

(pq)

p

q吸收律:p(pq)p；

p(pq)p同一律:p0p；

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

pq假言易位式:p→q

p→q第十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日15推理定律推理定律——重言蘊(yùn)涵式重要的推理定律A(AB)附加律(AB)A化簡(jiǎn)律(AB)AB假言推理(AB)B

A拒取式第十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日16推理定律(AB)BA析取三段論(AB)(BC)(AC)假言三段論(AB)(BC)(AC)等價(jià)三段論(AB)(CD)(AC)(BD)構(gòu)造性二難(AB)(AB)(AA)B構(gòu)造性二難(特殊形式)(AB)(CD)(BD)(AC)破壞性二難

第十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日17在自然推理系統(tǒng)P中構(gòu)造證明1.直接證明法例用構(gòu)造證明法構(gòu)造下面推理的證明:若明天是星期一或星期三,我就有課.若有課,今天必備課.我今天下午沒(méi)備課.所以,說(shuō)明天是星期一或星期三是不對(duì)的.

構(gòu)造證明設(shè)p:明天是星期一,q:明天是星期三,r:我有課,s:我備課形式結(jié)構(gòu)前提:(pq)r,rs,s結(jié)論:pq第十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日18證明①rs前提引入②s前提引入③r①②拒取式④(pq)r前提引入⑤(pq)③④拒取式⑥pq⑤置換第十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日192.附加前提證明法(1)欲證:前提:A1,A2,…,Ak結(jié)論:CB(2)等價(jià)地證明前提:A1,A2,…,Ak,C結(jié)論:B(3)理由:(A1A2…Ak)(CB)

(A1A2…Ak)(CB)

(A1A2…AkC)B(A1A2…AkC)B第十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日20例:構(gòu)造下面推理的證明2是素?cái)?shù)或合數(shù).若2是素?cái)?shù),則21/2是無(wú)理數(shù).若21/2是無(wú)理數(shù),則4不是素?cái)?shù).所以,如果4是素?cái)?shù),則2是合數(shù).用附加前提證明法構(gòu)造證明(1)設(shè)p:2是素?cái)?shù),q:2是合數(shù),r:21/2是無(wú)理數(shù),s:4是素?cái)?shù)(2)形式結(jié)構(gòu)前提:pq,pr,rs結(jié)論:sq第二十頁(yè)，共一百四十八頁(yè)，2022年，8月28日21(3)證明①s附加前提引入②pr前提引入③rs前提引入④ps②③假言三段論⑤p①④拒取式⑥pq前提引入⑦q⑤⑥析取三段論第二十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日223.歸謬法(或稱反證法)(1)欲證A1A2…AkB前提:A1,A2,…,Ak

結(jié)論:B(2)將B當(dāng)前提,推出矛盾,得證(1)正確(3)理由 A1A2…AkB

(A1A2…Ak)B

(A1A2…AkB)括號(hào)內(nèi)部為矛盾式當(dāng)且僅當(dāng)(A1A2…AkB)為重言式第二十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日23例:前提:(pq)r,rs,s,p

結(jié)論:q證明(用歸繆法)①q結(jié)論否定引入②rs前提引入③s前提引入④r②③拒取式⑤(pq)r前提引入⑥(pq)④⑤析取三段論⑦pq⑥置換⑧p①⑦析取三段論⑨p前提引入⑩

pp⑧⑨合取第二十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日24命題邏輯的歸結(jié)法基本單元：簡(jiǎn)單命題(陳述句)例：

命題：A1、A2、A3

和B求證：A1A2A3成立,則B成立,即：A1A2A3→B反證法：證明A1A2A3

B是矛盾式

(永假式)第二十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日25命題邏輯的歸結(jié)法建立子句集合取范式：命題、命題或的與,如：

P∧(P∨Q)∧(～P∨Q)子句集S：合取范式形式下的子命題(元素)的集合例：命題公式：P∧(P∨Q)∧(～P∨Q)

子句集S：S={P,P∨Q,～P∨Q}第二十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日26命題邏輯的歸結(jié)法歸結(jié)式消除互補(bǔ)文字對(duì),求新子句→得到歸結(jié)式。如子句：C1=C1'∨L,C2=C2'∨～L,

歸結(jié)式：R(C1,C2)=C1'∨C2'

注意：C1∧C2→R(C1,C2),反之不一定成立。第二十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日27命題邏輯的歸結(jié)法歸結(jié)過(guò)程

將命題寫成合取范式求出子句集對(duì)子句集使用歸結(jié)推理規(guī)則歸結(jié)式作為新子句參加歸結(jié)歸結(jié)式為空子句□,S是不可滿足的(矛盾),原命題成立。?(證明完畢)謂詞的歸結(jié)：除了有量詞和函數(shù)以外,其余和命題歸結(jié)過(guò)程一樣。第二十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日28命題邏輯歸結(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}第二十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日29命題邏輯歸結(jié)例題(2)子句集為： {～P∨Q,～Q,P}(4)對(duì)子句集中的子句進(jìn)行歸結(jié)可得：1.

～P∨Q2.

～Q3.

P4.

Q, (1,3歸結(jié))5.

, (2,4歸結(jié))

由上可得原公式成立。第二十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日30第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第三十頁(yè)，共一百四十八頁(yè)，2022年，8月28日31第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第三十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日32謂詞歸結(jié)原理基礎(chǔ)一階邏輯基本概念個(gè)體詞：表示主語(yǔ)的詞謂詞：刻畫個(gè)體性質(zhì)或個(gè)體之間關(guān)系的詞量詞：表示數(shù)量的詞第三十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日33謂詞歸結(jié)原理基礎(chǔ)小王是個(gè)工程師。8是個(gè)自然數(shù)。我去買花。小麗和小華是朋友。其中,“小王”、“工程師”、“我”、“花”、“8”、“小麗”、“小華”都是個(gè)體詞,而“是個(gè)工程師”、“是個(gè)自然數(shù)”、“去買”、“是朋友”都是謂詞。顯然前兩個(gè)謂詞表示的是事物的性質(zhì),第三個(gè)謂詞“去買”表示的一個(gè)動(dòng)作也表示了主、賓兩個(gè)個(gè)體詞的關(guān)系,最后一個(gè)謂詞“是朋友”表示兩個(gè)個(gè)體詞之間的關(guān)系。第三十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日34謂詞歸結(jié)原理基礎(chǔ)一階邏輯公式及其解釋個(gè)體常量：a,b,c個(gè)體變量：x,y,z謂詞符號(hào)：P,Q,R量詞符號(hào)：

,第三十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日35謂詞歸結(jié)原理基礎(chǔ)例如：(1)所有的人都是要死的。

(2)

有的人活到一百歲以上。在個(gè)體域D為人類集合時(shí),可符號(hào)化為：(1)xP(x),其中P(x)表示x是要死的。(2)xQ(x),其中Q(x)表示x活到一百歲以上。在個(gè)體域D是全總個(gè)體域時(shí),引入特殊謂詞R(x)表示x是人,可符號(hào)化為：(1)x(R(x)→P(x)),

其中,R(x)表示x是人；P(x)表示x是要死的。(2)x(R(x)∧Q(x)),

其中,R(x)表示x是人；Q(x)表示x活到一百歲以上。第三十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日36謂詞歸結(jié)原理基礎(chǔ)量詞否定等值式：～(x

)

M(x)(y

)～

M(y)～(x

)

M(x)(y

)～

M(y)量詞分配等值式：(x

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

)

P(x)∧(x

)

Q(x)(x

)(P(x)∨Q(x))(x

)

P(x)∨(x

)

Q(x)消去量詞等值式：設(shè)個(gè)體域?yàn)橛懈F集合(a1,a2,…an)(x

)

P(x)P(a1)∧P(a2)∧…∧P(an)(x

)P(x)P(a1)∨P(a2)∨…∨P(an)第三十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日37一階(firstorder)邏輯的合式公式項(xiàng)原子公式合式公式第三十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日38項(xiàng)(term)個(gè)體常項(xiàng)和個(gè)體變項(xiàng)是項(xiàng)若(x1,x2,…,xn)是n元函數(shù),t1,t2,…,tn是項(xiàng),則(t1,t2,…,tn)是項(xiàng)所有的項(xiàng)都是有限次地應(yīng)用上述規(guī)則形成的例如:a,x,f(a),g(a,x),g(x,f(a))第三十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日39原子公式(atomicformula)若R(x1,x2,…,xn)是n元謂詞,t1,t2,…,tn是項(xiàng),則R(t1,t2,…,tn)是原子公式例如:F(a),G(a,y),F(f(a)),G(x,g(a,y))第三十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日40合式公式(well-formedformula)原子公式是合式公式若A是合式公式,則(?A)是合式公式若A,B是合式公式,則(A∧B),(A∨B),(A→B),(A?B)也是合式公式若A是合式公式,則xA,xA也是合式公式只有有限次地應(yīng)用上述規(guī)則形成的符號(hào)串才是合式公式第四十頁(yè)，共一百四十八頁(yè)，2022年，8月28日41合式公式(舉例)x(F(x)y(G(y)H(x,y)))F(f(a,a),b)約定：省略多余括號(hào)最外層優(yōu)先級(jí)遞減：,;

?;∧,∨;→,?第四十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日42合式公式中的變項(xiàng)量詞轄域:在xA,xA中,A是量詞的轄域.例如:x(F(x)y(G(y)H(x,y)))指導(dǎo)變項(xiàng):緊跟在量詞后面的個(gè)體變項(xiàng).例如:x(F(x)y(G(y)H(x,y)))約束出現(xiàn):在轄域中與指導(dǎo)變項(xiàng)同名的變項(xiàng).例如:x(F(x)y(G(y)H(x,y)))自由出現(xiàn):既非指導(dǎo)變項(xiàng)又非約束出現(xiàn).例如:y(G(y)H(x,y))第四十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日43合式公式中的變項(xiàng)(舉例)H(x,y)∨xF(x)∨y(G(y)H(x,y))x與y是指導(dǎo)變項(xiàng)x與y是約束出現(xiàn)x與y是自由出現(xiàn)第四十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日44換名(rename)規(guī)則把某個(gè)指導(dǎo)變項(xiàng)和其量詞轄域中所有同名的約束出現(xiàn),都換成某個(gè)新的個(gè)體變項(xiàng)符號(hào).例如:x(A(x)∧B(x))y(A(y)∧B(y))xA(x)∧xB(x)yA(y)∧zB(z)H(x,y)∨xF(x)∨y(G(y)H(x,y))H(x,y)∨zF(z)∨u(G(u)H(x,u))第四十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日45代替(substitute)規(guī)則把某個(gè)自由變項(xiàng)的所有出現(xiàn),都換成某個(gè)新的個(gè)體變項(xiàng)符號(hào).例如:A(x)∧B(x)A(y)∧B(y)xA(x)∧B(x)xA(x)∧B(y)H(x,y)∨xF(x)∨y(G(y)H(x,y))H(s,t)∨xF(x)∨y(G(y)H(s,y))第四十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日46解釋(interpret)對(duì)一個(gè)合式公式的解釋包括給出個(gè)體域謂詞函數(shù)個(gè)體常項(xiàng)的具體含義第四十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日47解釋(舉例)F(f(a,a),b)解釋1：個(gè)體域是全體自然數(shù);a:2;b:4;f(x,y)=x+y;F(x,y):x=y

原公式解釋成:“2+2=4”。解釋2：個(gè)體域是全體實(shí)數(shù);a:3;b:5;f(x,y)=x-y;F(x,y):x>y

原公式解釋成:“3-3>5”。第四十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日48謂詞歸結(jié)原理基礎(chǔ)量詞分配等值式①x(A(x)B(x))

xA(x)xB(x)②x(A(x)B(x))

xA(x)xB(x)注意:對(duì)無(wú)分配律,對(duì)無(wú)分配律第四十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日49量詞分配(反例)x(A(x)∨B(x))xA(x)∨xB(x)x(A(x)∨B(x))xA(x)∨xB(x)

個(gè)體域?yàn)槿w自然數(shù);A(x):x是偶數(shù)

B(x):x是奇數(shù);左1,右0x(A(x)∧B(x))

xA(x)∧xB(x)x(A(x)∧B(x))

xA(x)∧xB(x)

個(gè)體域?yàn)槿w自然數(shù);A(x):x是偶數(shù)

B(x):x是奇數(shù);左0,右1第四十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日50謂詞歸結(jié)原理基礎(chǔ)量詞轄域收縮與擴(kuò)張等值式：(x

)(P(x)∨Q)(x

)

P(x)∨Q(x

)(P(x)∧Q)(x

)

P(x)∧Q(x

)(P(x)→Q)(x

)

P(x)→Q(x

)(Q

→P(x))Q→(x

)

P(x)(x

)(P(x)∨Q)(x

)

P(x)∨Q(x

)(P(x)∧Q)(x

)

P(x)∧Q(x

)(P(x)→Q)(x

)

P(x)→Q(x

)(Q

→P(x))Q→(x

)

P(x)第五十頁(yè)，共一百四十八頁(yè)，2022年，8月28日51前束范式前束范式與公式的前束范式1.前束范式定義設(shè)A為一個(gè)一階邏輯公式,若A具有如下形式Q1x1Q2x2…QkxkB則稱A為前束范式,其中Qi(1ik)為或,B為不含量詞的公式.例如,x(F(x)y(G(y)H(x,y)))不是前束范式,xy(F(x)(G(y)H(x,y)))是前束范式.又如,x(F(x)G(x))不是前束范式,x(F(x)G(x))是前束范式.第五十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日522.公式的前束范式定理(前束范式存在定理)一階邏輯中的任何公式都存在與之等值的前束范式(不惟一)3.如何求公式的前束范式利用重要等值式、置換規(guī)則、換名規(guī)則、代替規(guī)則進(jìn)行等值演算第五十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日53例求下列公式的前束范式(1)x(M(x)F(x))(2)xF(x)xG(x)(3)xF(x)xG(x)(4)xF(x)y(G(x,y)H(y))(5)x(F(x,y)y(G(x,y)H(x,z)))解(1)x(M(x)F(x))

x(M(x)F(x))(量詞否定等值式)

x(M(x)F(x))兩步結(jié)果都是前束范式,說(shuō)明不惟一性.第五十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日54(2)xF(x)xG(x)

xF(x)xG(x)(量詞否定等值式)

x(F(x)G(x))(量詞分配等值式)另有一種形式

xF(x)xG(x)

xF(x)xG(x)

xF(x)yG(y)

xy(F(x)G(y))兩種形式是等值的第五十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日55(3)xF(x)xG(x)

xF(x)xG(x)

x(F(x)G(x))(為什么？)或

xy(F(x)G(y))(為什么？)第五十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日56(4)xF(x)y(G(x,y)H(y))

zF(z)y(G(x,y)H(y))(換名規(guī)則)

zy(F(z)(G(x,y)H(y)))(為什么?)或

xF(x)y(G(z,y)H(y))(代替規(guī)則)

xy(F(x)(G(z,y)H(y)))第五十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日57(5)可用換名規(guī)則,也可用代替規(guī)則,這里用代替規(guī)則

x(F(x,y)y(G(x,y)H(x,z)))

x(F(x,u)y(G(x,y)H(x,z)))

xy(F(x,u)G(x,y)H(x,z)))注意:x與y不能顛倒第五十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日58謂詞推理(舉例)前提:x(F(x)G(x)),F(a)

結(jié)論:G(a)

證明:(1)F(a)前提引入

(2)x(F(x)G(x))前提引入

(3)F(a)G(a)(2)UI(4)G(a)(1)(3)假言推理第五十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日59謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)SKOLEM標(biāo)準(zhǔn)形前束范式說(shuō)公式A是一個(gè)前束范式,如果A中的一切量詞都位于該公式的最左邊(不含否定詞),且這些量詞的轄域都延伸到公式的末端。第五十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日60謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)即：把所有的量詞都提到前面去,然后消掉所有量詞

(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)約束變項(xiàng)換名規(guī)則：(Qx

)

M(x)(Qy

)

M(y)(Qx

)

M(x,z)

(Qy

)

M(y,z)第六十頁(yè)，共一百四十八頁(yè)，2022年，8月28日61謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)

量詞消去原則：消去存在量詞“”,略去全程量詞“”。

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

第六十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日62謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)Skolem定理：謂詞邏輯的任意公式都可以化為與之等價(jià)的前束范式,但其前束范式不唯一。SKOLEM標(biāo)準(zhǔn)形定義：消去量詞后的謂詞公式。注意：謂詞公式G的SKOLEM標(biāo)準(zhǔn)形同G并不等值。第六十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日63謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)例:將下式化為Skolem標(biāo)準(zhǔn)形：～((x)(y)P(a,x,y)→(x)(～(y)Q(y,b)→R(x)))解：第一步,消去→號(hào),得： ～(～(x)(y)P(a,x,y))∨(x)(～～(y)Q(y,b)∨R(x))第二步,～深入到量詞內(nèi)部,得：

(x)(y)P(a,x,y)∧～(x)((y)Q(y,b)∨R(x))(x)(y)P(a,x,y)∧(x)((y)(～Q(y,b)∧～R(x))第六十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日64謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)第三步,任意量詞左移(分配律),變?cè)酌?得

(x)((y)P(a,x,y)∧(z)(～Q(z,b)∧～R(x))第四步,存在量詞左移,直至所有的量詞移到前面,得：(x)(y)(z)P(a,x,y)∧～Q(z,b)∧～R(x))由此得到前束范式第六十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日65謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)第五步,消去“”(存在量詞),略去“”全稱量詞消去(y),因?yàn)樗筮呏挥?x),所以使用x的函數(shù)f(x)代替之,這樣得到：

(x)(z)(P(a,x,f(x))∧～Q(z,b)∧～R(x))

消去(z),同理使用g(x)代替之,這樣得到：

(x)(P(a,x,f(x))∧～Q(g(x),b)∧～R(x))

則,略去全稱變量,原式的Skolem標(biāo)準(zhǔn)形為：

P(a,x,f(x))∧～Q(g(x),b)∧～R(x)

第六十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日66謂詞歸結(jié)子句形子句與子句集文字：不含任何連接詞的謂詞公式。子句：一些文字的析取(謂詞的和)。子句集S的求?。篏→SKOLEM標(biāo)準(zhǔn)形消去存在變量以“,”取代“∧”,并表示為集合形式。第六十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日67謂詞歸結(jié)子句形

G是不可滿足的S是不可滿足的G與S不等價(jià),但在不可滿足得意義下是一致的。定理： 若G是給定的公式,而S是相應(yīng)的子句集,則G是不可滿足的S是不可滿足的。

注意：G真不一定S真,而S真必有G真。 即：S

G第六十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日68謂詞歸結(jié)子句形G=G1∧G2∧G3∧…∧Gn

的子句形G的字句集可以分解成幾個(gè)單獨(dú)處理。

有SG=S1US2US3U…USn

則SG

與S1US2US3U…USn在不可滿足得意義上是一致的。 即SG

不可滿足S1US2US3U…USn不可滿足第六十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日69求取子句集例(1)例：對(duì)所有的x,y,z來(lái)說(shuō),如果y是x的父親,z又是y的父親,則z是x的祖父。又知每個(gè)人都有父親,試問(wèn)對(duì)某個(gè)人來(lái)說(shuō)誰(shuí)是它的祖父？求：用一階邏輯表示這個(gè)問(wèn)題,并建立子句集。解：這里我們首先引入謂詞：

P(x,y)表示x是y的父親

Q(x,y)表示x是y的祖父

ANS(x)表示問(wèn)題的解答第六十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日70求取子句集例(2)對(duì)于第一個(gè)條件,“如果x是y的父親,y又是z的父親,則x是z的祖父”,一階邏輯表達(dá)式如下：A1：(x)(y)(z)(P(x,y)∧P(y,z)→Q(x,z))SA1：～P(x,y)∨～P(y,z)∨Q(x,z)對(duì)于第二個(gè)條件：“每個(gè)人都有父親”,一階邏輯表達(dá)式：A2：(y)(x)P(x,y)SA2：P(f(y),y)第七十頁(yè)，共一百四十八頁(yè)，2022年，8月28日71求取子句集例(2)對(duì)于結(jié)論：某個(gè)人是它的祖父B：(x)(y)Q(x,y)否定后得到子句：～((x)(y)Q(x,y))∨ANS(x)S～B：～Q(x,y)∨ANS(x)則得到的相應(yīng)的子句集為：{SA1,SA2,S～B}第七十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日72第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第七十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日73第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第七十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日74歸結(jié)原理歸結(jié)原理正確性的根本在于,找到矛盾可以肯定不真。方法：和命題邏輯一樣。但由于有函數(shù),所以要考慮合一和置換。第七十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日75置換置換：可以簡(jiǎn)單的理解為是在一個(gè)謂詞公式中用置換項(xiàng)去置換變量。定義：置換是形如{t1/x1,t2/x2,…,tn/xn}的有限集合。其中,x1,x2,…,xn是互不相同的變量,t1,t2,…,tn是不同于xi的項(xiàng)(常量、變量、函數(shù))；ti/xi表示用ti置換xi,并且要求ti與xi不能相同,而且xi不能循環(huán)地出現(xiàn)在另一個(gè)ti中。例如{a/x,c/y,f(b)/z}是一個(gè)置換。{g(y)/x,f(x)/y}不是一個(gè)置換,

第七十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日76置換的合成設(shè)＝{t1/x1,t2/x2,…,tn/xn}, ＝{u1/y1,u2/y2,…,un/yn},是兩個(gè)置換。 則與的合成也是一個(gè)置換,記作·。它是從集合

{t1·/x1,t2·/x2,…,tn·/xn,u1/y1,u2/y2,…,un/yn}

中刪去以下兩種元素：當(dāng)ti·

=xi時(shí),刪去ti·

/xi(i=1,2,…,n);

當(dāng)yi{x1,x2,…,xn}時(shí),刪去uj/yj(j=1,2,…,m)

最后剩下的元素所構(gòu)成的集合。合成即是對(duì)ti先做置換然后再做置換,置換xi第七十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日77置換的合成例：設(shè)：＝{f(y)/x,z/y},＝{a/x,b/y,y/z},求與的合成。解：先求出集合

{f(b/y)/x,(y/z)/y,a/x,b/y,y/z}＝{f(b)/x,y/y,a/x,b/y,y/z}

其中,f(b)/x中的f(b)是置換作用于f(y)的結(jié)果；y/y中的y是置換作用于z的結(jié)果。在該集合中,y/y滿足定義中的條件i,需要?jiǎng)h除；a/x,b/y滿足定義中的條件ii,也需要?jiǎng)h除。最后得

·＝{f(b)/x,y/z}第七十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日78合一合一可以簡(jiǎn)單地理解為“尋找相對(duì)變量的置換,使兩個(gè)謂詞公式一致”。定義：設(shè)有公式集F＝{F1,F2,…,Fn},若存在一個(gè)置換,可使F1＝F2＝…=Fn,則稱是F的一個(gè)合一。同時(shí)稱F1,F2,...,Fn是可合一的。

例： 設(shè)有公式集F＝{P(x,y,f(y)),P(a,g(x),z)},則＝{a/x,g(a)/y,f(g(a))/z}是它的一個(gè)合一。注意：一般說(shuō)來(lái),一個(gè)公式集的合一不是唯一的。

第七十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日79歸結(jié)原理歸結(jié)的注意事項(xiàng)：謂詞的一致性,P()與Q(),不可以常量的一致性,P(a,…)與P(b,….),不可以 變量,P(a,….)與P(x,…),可以變量與函數(shù),P(a,x,….)與P(x,f(x),…),不可以；是不能同時(shí)消去兩個(gè)互補(bǔ)對(duì),P∨Q與～P∨～Q的空,不可以先進(jìn)行內(nèi)部簡(jiǎn)化(置換、合并)

第七十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日80歸結(jié)原理歸結(jié)的過(guò)程寫出謂詞關(guān)系公式→用反演法寫出謂詞表達(dá)式→SKOLEM標(biāo)準(zhǔn)形→子句集S→對(duì)S中可歸結(jié)的子句做歸結(jié)→歸結(jié)式仍放入S中,反復(fù)歸結(jié)過(guò)程→得到空子句命題得證第八十頁(yè)，共一百四十八頁(yè)，2022年，8月28日81例題“快樂(lè)學(xué)生”問(wèn)題假設(shè)任何通過(guò)計(jì)算機(jī)考試并獲獎(jiǎng)的人都是快樂(lè)的,任何肯學(xué)習(xí)或幸運(yùn)的人都可以通過(guò)所有的考試,張不肯學(xué)習(xí)但他是幸運(yùn)的,任何幸運(yùn)的人都能獲獎(jiǎng)。求證：張是快樂(lè)的。解：先將問(wèn)題用謂詞表示如下：R1:“任何通過(guò)計(jì)算機(jī)考試并獲獎(jiǎng)的人都是快樂(lè)的”(x)((Pass(x,computer)∧Win(x,prize))→Happy(x))第八十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日82例題“快樂(lè)學(xué)生”問(wèn)題R2:“任何肯學(xué)習(xí)或幸運(yùn)的人都可以通過(guò)所有考試”(x)(y)(Study(x)∨Lucky(x)→Pass(x,y))R3:“張不肯學(xué)習(xí)但他是幸運(yùn)的”～Study(zhang)∧Lucky(zhang)R4:“任何幸運(yùn)的人都能獲獎(jiǎng)”(x)(Lucky(x)→Win(x,prize))結(jié)論：“張是快樂(lè)的”的否定～Happy(zhang)第八十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日83例題“快樂(lè)學(xué)生”問(wèn)題由R1及邏輯轉(zhuǎn)換公式:P∧W→H=～(P∧W)∨H,可得(1)～Pass(x,computer)∨～Win(x,prize)∨Happy(x)由R2(變量更名處理)：(2)～Study(y)∨Pass(y,z)(3)～Lucky(u)∨Pass(u,v)由R3：(4)～Study(zhang)(5)Lucky(zhang)由R4(變量更名處理)

：(6)～Lucky(w)∨Win(w,prize)由結(jié)論(否定)：(7)～Happy(zhang) (結(jié)論的否定)第八十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日84例題“快樂(lè)學(xué)生”問(wèn)題(8)～Pass(w,computer)∨Happy(w)∨～Luck(w)(1)(6),{w/x}(9)～Pass(zhang,computer)∨～Lucky(zhang)(8)(7),{zhang/w}(10)

～Pass(zhang,computer) (9)(5)(11)

～Lucky(zhang) (10)(3),{zhang/u,computer/v}(12)

(11)(5)

第八十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日85歸結(jié)原理歸結(jié)法的實(shí)質(zhì)：歸結(jié)法是僅有一條推理規(guī)則的推理方法。歸結(jié)的過(guò)程是一個(gè)語(yǔ)義樹倒塌的過(guò)程。歸結(jié)法的問(wèn)題子句中有等號(hào)或不等號(hào)時(shí),完備性不成立?！鵋erbrand定理的不實(shí)用性引出了可實(shí)用的歸結(jié)法。第八十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日86第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第八十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日87第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第八十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日88歸結(jié)過(guò)程的控制策略要解決的問(wèn)題：歸結(jié)方法的知識(shí)爆炸。控制策略的目的歸結(jié)點(diǎn)盡量少控制策略的原則給出控制策略,以使僅對(duì)選擇合適的子句間方可做歸結(jié)。避免多余的、不必要的歸結(jié)式出現(xiàn)?；蛘哒f(shuō),少做些歸結(jié)仍能導(dǎo)出空子句。第八十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日89例:

S＝{P∨Q,～P∨Q，P∨～Q,～P∨～Q}來(lái)證明是不滿足的。

證明過(guò)程是從S0＝S出發(fā)。依次構(gòu)造

Si={C1,C2的歸結(jié)式C1S0∪S1…∪Si-1,C2Si-1}i=1,2,…,直至出現(xiàn)空子句□證明結(jié)束。這就是盲目全面歸結(jié)的描述。具體的歸結(jié)過(guò)程是

S0(1)P∨Q

(2)～P∨Q

(3)P∨～Q

(4)～P∨～Q

S1(5)Q

(1)(2)

(6)P

(1)(3)

(7)Q∨～Q(1)(4)

(8)P∨～P

(1)(4)

(9)Q∨～Q(2)(3)

(10)P∨～P

(2)(3)

(11)～P(2)(4)

(12)～Q

(3)(4)

第八十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日90

S2(13)P∨Q(1)(7)

(14)P∨Q

(1)(8)

(15)P∨Q(1)(9)

(16)P∨Q

(1)(10)

(17)Q(1)(11)

(18)P

(1)(12)

(19)Q(2)(6)

(20)～P∨Q

(2)(7)

(21)～P∨Q(2)(8)

(22)～P∨Q

(2)(9)

(23)～P∨Q(2)(10)

(24)～P

(2)(12)

(25)P(3)(5)

(26)P∨～Q

(3)(7)

(27)P∨～Q(3)(8)

(28)P∨～Q

(3)(9)

(29)P∨～Q

(3)(10)(30)～Q

(3)(11)

(31)～P(4)(5)

(32)～Q

(4)(6)

(33)～P∨～Q(4)(7)

(34)～P∨～Q

(4)(8)

(35)～P∨～Q(4)(9)(36)～P∨～Q

(4)(10)

(37)Q(5)(7)

(38)Q

(5)(9)

(39)□(5)(12)第九十頁(yè)，共一百四十八頁(yè)，2022年，8月28日91在這種歸結(jié)過(guò)程中產(chǎn)生了相當(dāng)數(shù)量的不必要的歸結(jié)式。一類是重言式如(7)－(10)，由它們又產(chǎn)生了歸結(jié)式(13)―(16)，(20)－(23)，(26)―(29)，(33)－(39)。另一類是重復(fù)的，如P,Q,～P,～Q就多次出現(xiàn)過(guò)。

就這個(gè)例子而言，若由人來(lái)證明只需三步，(5)(12)(39)便得空子句，這節(jié)將介紹刪除策略、語(yǔ)義歸結(jié)和線性歸結(jié)等控制策略。第九十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日92控制策略的方法(1)

刪除策略 完備名詞解釋：歸類：設(shè)有兩個(gè)子句C和D,若有置換使得C

D成立,則稱子句C把子句D歸類。

由于小的可以代表大的,所以小的吃掉大的了。若對(duì)S使用歸結(jié)推理過(guò)程中,當(dāng)歸結(jié)式Cj是重言式(永真式)和Cj被S中子句和子句集的歸結(jié)式Ci(i<j)所歸類時(shí),便將Cj刪除。這樣的推理過(guò)程便稱做使用了刪除策略的歸結(jié)過(guò)程。第九十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日93控制策略的方法(1)主要思想：歸結(jié)過(guò)程在尋找可歸結(jié)子句時(shí),子句集中的子句越多,需要付出的代價(jià)就會(huì)越大。如果在歸結(jié)時(shí)能把子句集中無(wú)用的子句刪除掉,就會(huì)縮小搜索范圍,減少比較次數(shù),從而提高歸結(jié)效率。刪除策略對(duì)阻止不必要的歸結(jié)式的產(chǎn)生來(lái)縮短歸結(jié)過(guò)程是有效的。然而要在歸結(jié)式Cj產(chǎn)生后方能判別它是否可被刪除,這部分計(jì)算量是要花費(fèi)的,只是節(jié)省了被刪除的子句又生成的歸結(jié)式。盡管使用刪除策略的歸結(jié),少做了歸結(jié)但不影響產(chǎn)生空子句,就是說(shuō)刪除策略的歸結(jié)推理是完備的。第九十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日94控制策略的方法(2)采用支撐集 完備支撐集：設(shè)有不可滿足子句集S的子集T,如果S-T是可滿足的,則T是支持集。采用支撐集策略時(shí),從開始到得到的整個(gè)歸結(jié)過(guò)程中,只選取不同時(shí)屬于S-T的子句,在其間進(jìn)行歸結(jié)。就是說(shuō),至少有一個(gè)子句來(lái)自于支撐集T或由T導(dǎo)出的歸結(jié)式。第九十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日95例如：A1∧A2∧A3∧～B中的～B可以作為支撐集使用。要求每一次參加歸結(jié)的親本子句中,只要應(yīng)該有一個(gè)是有目標(biāo)公式的否定(～B)所得到的子句或者它們的后裔。支撐集策略的歸結(jié)是完備的,同樣,所有可歸結(jié)的謂詞公式都可以用采用支撐集策略達(dá)到加快歸結(jié)速度的目的。問(wèn)題是如何尋找合適的支撐集。一個(gè)最容易找到的支撐集是目標(biāo)子句的非,即S～B。

第九十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日96例:

S＝{P∨Q,～P∨R,～Q∨R，～R}

取T＝{～R}

支持集歸結(jié)過(guò)程

(1)P∨Q

(2)～P∨R

(3)～Q∨R

(4)～R

(5)～P

(2)(4)

(6)～Q

(3)(4)

(7)Q

(1)(5)

(8)P

(1)(6)

(9)R

(3)(7)

(10)□

(6)(7)第九十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日97ST可滿足支撐集示意圖第九十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日98控制策略的方法(3)

語(yǔ)義歸結(jié) 完備 語(yǔ)義歸結(jié)策略是將子句S按照一定的語(yǔ)義分成兩部分,約定每部分內(nèi)的子句間不允許作歸結(jié)。同時(shí)還引入了文字次序,約定歸結(jié)時(shí)其中的一個(gè)子句的被歸結(jié)文字只能是該子句中“最大”的文字。

第九十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日99控制策略的方法(3)

語(yǔ)義歸結(jié)策略的歸結(jié)是完備的,同樣,所有可歸結(jié)的謂詞公式都可以用采用語(yǔ)義歸結(jié)策略達(dá)到加快歸結(jié)速度的目的。問(wèn)題是如何尋找合適的語(yǔ)義分類方法,并根據(jù)其含義將子句集兩個(gè)部分中的子句進(jìn)行排序。

第九十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日100例:

S＝{～P∨～Q∨R,P∨R,Q∨R,～R}.我們先規(guī)定S中出現(xiàn)的文字的次序，如依次為P，Q，R或記作P>Q>R。再選取S的一個(gè)解釋I，如令

I＝{～P,～Q,～R}

用它來(lái)將S分成兩個(gè)部分。規(guī)定在I下為假的子句放入S1中，在I下為真的子句放入S2中。于是有

S1={P∨R,Q∨R}

S2＝{～P∨～Q∨R,～R}

規(guī)定S1內(nèi)部的子句不允許歸結(jié)，S1與S2子句間的歸結(jié)必須是S中的最大文字方可進(jìn)行。這樣所得的歸結(jié)式，仍按I來(lái)放入S1或S2。第一百頁(yè)，共一百四十八頁(yè)，2022年，8月28日101歸結(jié)過(guò)程

(1)～P∨～Q∨RS2

(2)P∨RS1

(3)Q∨RS1

(4)～RS2

(5)～Q∨R

(2)(1)歸結(jié)

S2

(6)～P∨R

(3)(1)歸結(jié)

S2

(7)R

(2)(6)歸結(jié)

S1

(8)R

(3)(5)歸結(jié)

S1

(9)□

(7)(4)歸結(jié)

這是采用了語(yǔ)義歸結(jié)策略下的盲目全面歸結(jié)過(guò)程。明顯地減少歸結(jié)次數(shù)。阻止了(1)(4)的歸結(jié)，也阻止了(2)(4)的歸結(jié)。第一百零一頁(yè)，共一百四十八頁(yè)，2022年，8月28日102控制策略的方法(4)

線性歸結(jié)完備線性歸結(jié)策略首先從子句集中選取一個(gè)稱作頂子句的子句C0開始作歸結(jié)。歸結(jié)過(guò)程中所得到的歸結(jié)式Ci立即同另一子句Bi進(jìn)行歸結(jié)得歸結(jié)式Ci+1。而Bi屬于S或是已出現(xiàn)的歸結(jié)式Cj(j<i)。即,如下圖所示歸結(jié)得到的新子句立即參加歸結(jié)。第一百零二頁(yè)，共一百四十八頁(yè)，2022年，8月28日103C0B0B1B2C1C2空線性歸結(jié)策略示意圖第一百零三頁(yè)，共一百四十八頁(yè)，2022年，8月28日104例:

S＝{P∨Q,～P∨Q,P∨～Q,～P∨～Q}

選取頂子句C0＝P∨Q。

線性歸結(jié)過(guò)程

(1)P∨Q

(2)～P∨Q

(3)P∨～Q

(4)～P∨～Q

(5)Q(1)(2)

(6)P(5)(3)

(7)～Q(6)(4)

(8)□(7)(5)

頂子句的選擇直接影響著歸結(jié)的效率。如可選得C0使S－{C0}是可滿足的。第一百零四頁(yè)，共一百四十八頁(yè)，2022年，8月28日105控制策略的方法(4)

線性歸結(jié)是完備的,同樣,所有可歸結(jié)的謂詞公式都可以采用線性歸結(jié)策略達(dá)到加快歸結(jié)速度的目的。如果能搞找到一個(gè)較好的頂子句,可以式歸結(jié)順利進(jìn)行。否則也可能事與愿違。

第一百零五頁(yè)，共一百四十八頁(yè)，2022年，8月28日106控制策略的方法(5)

單元?dú)w結(jié) 完備單元?dú)w結(jié)策略要求在歸結(jié)過(guò)程中,每次歸結(jié)都有一個(gè)子句是單元子句(只含一個(gè)文字的子句)或單元因子。顯而易見,詞中方法可以簡(jiǎn)單地削去另一個(gè)非單子句中的一個(gè)因子,使其長(zhǎng)度減少,構(gòu)成簡(jiǎn)單化,歸結(jié)效率較高。初始子句集中沒(méi)有單元子句時(shí),單元?dú)w結(jié)策略無(wú)效。所以說(shuō)“反之不成立”,即此問(wèn)題不能采用單元?dú)w結(jié)策略。

第一百零六頁(yè)，共一百四十八頁(yè)，2022年，8月28日107例:

S＝{P∨Q,～P∨R,～Q∨R,～R}

單元?dú)w結(jié)過(guò)程

(1)P∨Q

(2)～P∨R

(3)～Q∨R

(4)～R

(5)～P

(4)(2)

(6)～Q

(4)(3)

(7)Q

(5)(1)

(8)P

(6)(1)

(9)R

(7)(3)

(10)□

(7)(6)第一百零七頁(yè)，共一百四十八頁(yè)，2022年，8月28日108控制策略的方法(6)

輸入歸結(jié) 完備與單元?dú)w結(jié)策略相似,輸入歸結(jié)策略要求在歸結(jié)過(guò)程中,每一次歸結(jié)的兩個(gè)子句中必須有一個(gè)是S的原始子句。這樣可以避免歸結(jié)出的不必要的新子句加入歸結(jié),造成惡性循環(huán)?？梢詼p少不必要的歸結(jié)次數(shù)。第一百零八頁(yè)，共一百四十八頁(yè)，2022年，8月28日109例:

S＝{P∨Q,～P∨R,～Q∨R,～R}

輸入歸結(jié)過(guò)程

(1)P∨Q

(2)～P∨R

(3)～Q∨R

(4)～R

(5)Q∨R

(1)(2)

(6)R

(3)(5)

(7)□

(4)(6)第一百零九頁(yè)，共一百四十八頁(yè)，2022年，8月28日110控制策略的方法(6)

如同單元?dú)w結(jié)策略,不是所有的可歸結(jié)謂詞公式的最后結(jié)論都是可以從原始子句集中的得到的。簡(jiǎn)單的例子,歸結(jié)結(jié)束時(shí),即最后一個(gè)歸結(jié)式為空子句的條件是,參加歸結(jié)的雙方必須是兩個(gè)單元子句。原始子句集中沒(méi)有單元子句的謂詞公式一定不能采用輸入歸結(jié)策略。

第一百一十頁(yè)，共一百四十八頁(yè)，2022年，8月28日111第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第一百一十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日112第三章歸結(jié)推理方法概述命題邏輯的歸結(jié)法謂詞歸結(jié)子句形歸結(jié)原理歸結(jié)過(guò)程的策略控制Herbrand定理第一百一十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日113Herbrand定理問(wèn)題： 一階邏輯公式的永真性(永假性)的判定是否能在有限步內(nèi)完成？第一百一十三頁(yè)，共一百四十八頁(yè)，2022年，8月28日114Herbrand定理1936年圖靈(Turing)和邱吉(Church)互相獨(dú)立地證明了：

“沒(méi)有一般的方法使得在有限步內(nèi)判定一階邏輯的公式是否是永真(或永假)。但是如果公式本身是永真(或永假)的,那么就能在有限步內(nèi)判定它是永真(或永假)。對(duì)于非永真(或永假)的公式就不一定能在有限步內(nèi)得到結(jié)論。判定的過(guò)程將可能是不停止的?！?/p>

第一百一十四頁(yè)，共一百四十八頁(yè)，2022年，8月28日115Herbrand定理Herbrand的思想定義：公式G永真：對(duì)于G的所有解釋,G都為真。思想：尋找一個(gè)已給的公式是真的解釋。然而,如果所給定的公式的確是永假的,就沒(méi)有這樣的解釋存在,并且算法在有限步內(nèi)停止。第一百一十五頁(yè)，共一百四十八頁(yè)，2022年，8月28日116Herbrand定理H域H解釋語(yǔ)義樹結(jié)論：Herbrand定理第一百一十六頁(yè)，共一百四十八頁(yè)，2022年，8月28日117Herbrand定理H域H解釋語(yǔ)義樹結(jié)論：Herbrand定理第一百一十七頁(yè)，共一百四十八頁(yè)，2022年，8月28日118Herbrand定理(H域)基本方法：因?yàn)榱吭~是任意的,所討論的個(gè)體變量域D是任意的,所以解釋的個(gè)數(shù)是無(wú)限、不可數(shù)的。簡(jiǎn)化討論域。建立一個(gè)比較簡(jiǎn)單、特殊的域,使得只要在這個(gè)論域上,該公式是不可滿足的。此域稱為H域。第一百一十八頁(yè)，共一百四十八頁(yè)，2022年，8月28日119Herbrand定理(H域)設(shè)G是已給的公式，定義在論域D上，令H0是G中所出現(xiàn)的常量的集合。若G中沒(méi)有常量出現(xiàn)，就任取常量aD，而規(guī)定H0={a}。Hi=Hi-1∪{所有形如f(t1,…,tn)的元素}其中f(t1,…,tn)是出現(xiàn)于G中的任一函數(shù)符號(hào)，而t1,…,tn

是Hi-1的元素，i=1,2,…。規(guī)定H為G的H域(或說(shuō)是相應(yīng)的子句集S的H域)。不難看出，H域是直接依賴于G的最多只有可數(shù)個(gè)元素。第一百一十九頁(yè)，共一百四十八頁(yè)，2022年，8月28日120D域H域H域與D域關(guān)系示意圖第一百二十頁(yè)，共一百四十八頁(yè)，2022年，8月28日121H域例題例1:

S={P(a),～P(x)∨P(f(x))}依定義有H0={a}H1={a}∪{f(a)}={a,f(a)}H2={a,f(a)}∪{f(a),f(f(a))}={a,f(a),f(f(a))}

…H={a,f(a),f(f(a)),…}第一百二十一頁(yè)，共一百四十八頁(yè)，2022年，8月28日122H域例題例2:

S={～P(z),P(x)∨～Q(y)}依定義有H0={a}

a是論域D中一常量。H1=H0H2=H1…H={a}第一百二十二頁(yè)，共一百四十八頁(yè)，2022年，8月28日123H域例題例3:

S={P(f(x),a,g(y),b)}