第二章謂詞演算與消解(歸結(jié))原理

命題演算謂詞演算推理規(guī)則產(chǎn)生謂詞演算表達(dá)式應(yīng)用歸結(jié)原理經(jīng)典數(shù)理邏輯AI研究?jī)?nèi)容之一是推理，即研究怎樣使計(jì)算機(jī)獲得自動(dòng)推理的能力數(shù)理邏輯用數(shù)學(xué)方法研究各種推理中的邏輯問(wèn)題，以推理本身作為研究對(duì)象AI要使用邏輯推理，就必然涉及數(shù)理邏輯/數(shù)理邏輯的經(jīng)典部分—經(jīng)典的命題邏輯和一階謂詞邏輯，同時(shí)作為人工智能的知識(shí)表示方法和推理方法而存在；因此數(shù)理邏輯是人工智能的一個(gè)基礎(chǔ)2.1命題演算2.1.1符號(hào)和命題命題演算的符號(hào)：是命題符號(hào),命題符號(hào)代表命題，是關(guān)于現(xiàn)實(shí)世界的能分辨真假值的陳述句。命題符號(hào)：P，Q，R，S，T命題演算的符號(hào)：真值符號(hào)：true,false

聯(lián)結(jié)詞：∨，∧，~

，=>，＝通過(guò)聯(lián)結(jié)詞可把多個(gè)命題組成合成的命題，也稱為合式公式。2.1.2命題演算的語(yǔ)義2.1命題演算—如兩個(gè)命題表達(dá)式在任何真值指派下都有相同的值，則稱為是等價(jià)的（P29）表2.2所示的真值表證明：P=>Q與~P∨Q等價(jià)?！獙?duì)于命題表達(dá)式P，Q，R~(~P)=P;(P∨Q)＝(~P=>Q)否定律：~(P∨Q)＝(~P∧~Q)~(P∧Q)＝(~P∨~Q)分配律：P∨(Q∧R)＝(P∨Q)∧(P∨R)

分配律：P∧(Q∨R)＝(P∧Q)∨(P∧R)

交換律：(P∧Q)＝(Q∧P)

交換律：(P∨Q)＝(Q∨P)

結(jié)合律：((P∧Q)∧R)＝(P∧(Q∧R))

結(jié)合律：((P∨Q)∨R)＝(P∨(Q∨R))

置換律：(P=>Q)＝(~Q=>~P)2.1命題演算2.2謂詞演算命題演算中，P，Q代表一定的命題，如：P：星期四下雨而謂詞：Weather（X，Y）代表日期與天氣的關(guān)系Weather（Tuesday，Rain）

可以操縱命題演算表達(dá)式允許包含變?cè)猈eather（X，Rain）

2.2.1謂詞的語(yǔ)法和命題2.2謂詞演算謂詞演算的字母表組成：（1）英文字母組合，包括大寫與小寫（2）數(shù)字集合0,1,…,9（3）下劃線如：George,fires,bill,xxxx

謂詞演算符號(hào)包括：真值符號(hào)true和false。常元符號(hào),第一個(gè)字符為小寫字母的符號(hào)表達(dá)式。變?cè)?hào),第一個(gè)字符為大寫字母的符號(hào)表達(dá)式。函詞符號(hào),第一個(gè)字符為小寫字母的符號(hào)表達(dá)式,函詞有一個(gè)元數(shù),指出從定義域中映射到值域中的每個(gè)元素。2.2謂詞演算例：

likes(george,kate).likes(X,george).likes(george,susie).likes(X,X).likes(george,sarah,tuesday).friends(bill,richard).friends(bill,george).friends(father(david),father(andrew))helps(bill,george).helps(richard,bill).2.2謂詞演算原子命題：是一個(gè)n元謂詞，后跟n個(gè)項(xiàng)，用括號(hào)括起來(lái)并用逗號(hào)分開(kāi)。2.2.1謂詞的語(yǔ)法和命題與謂詞相關(guān)的一個(gè)正整數(shù)稱為元數(shù)或“參數(shù)數(shù)目”，具有相同的名但元數(shù)不同的謂詞是不同的。真值true和false也是原子命題。任何原子命題都能夠用邏輯操作符將其變成謂詞演算的命題。用的聯(lián)結(jié)詞也和命題演算一樣:∨,∧,~,=>和＝。當(dāng)一個(gè)變?cè)谝粋€(gè)命題中作為參數(shù)出現(xiàn)時(shí),它代表的是域中不特定的對(duì)象。謂詞演算包括兩個(gè)符號(hào),量詞（全稱量詞）和彐（存在量詞）,用于限定包含變?cè)拿}的含義。

2.2.1謂詞的語(yǔ)法和命題一個(gè)量詞后面緊跟著一個(gè)變?cè)鸵粋€(gè)命題。例如：

Xlikes(X,ice_cream).彐Yfriends(Y,peter).

全稱量詞

,表明命題對(duì)于變?cè)淖冇蛑械乃械闹刀紴檎?。存在量詞彐,表明該命題對(duì)于變?cè)淖冇蛑械囊恍┲禐檎?。例：命題2.2.1謂詞的語(yǔ)法和命題plus(two,three)equal(plus(two,three))彐xfoo(x,two,plus(two,three))∧equal(plus(two,three),five)2.2.2謂詞演算的語(yǔ)義(P34)表達(dá)式的真值依賴于常元、變?cè)⒅^詞、函詞到論域中的映射；在論域中的關(guān)系的真假?zèng)Q定了相應(yīng)表達(dá)式的真假。例如：friends(george,susie)friends(george,kate)2.2.2謂詞演算的語(yǔ)義(P34)一個(gè)論域D上的解釋：假設(shè)論域D是一個(gè)非空集合，在D上的一個(gè)解釋把論域D的實(shí)體指派給一個(gè)謂詞演算表達(dá)式的每一個(gè)常元、變?cè)?、謂詞及函詞符號(hào)，于是有：1）每一個(gè)常元指派了D的一個(gè)元素。2）對(duì)每一個(gè)變?cè)?，指派D的一個(gè)非空集合，這是該變?cè)淖冇颉?）每個(gè)n元謂詞P定義在論域D中的n個(gè)參數(shù)上，并定義了從Dn到{T，F(xiàn)}的一個(gè)映射。4)每個(gè)m元函詞f定義在論域D的m個(gè)參數(shù)上，并定義了從Dm到{T，F(xiàn)}的一個(gè)映射。在一種解釋下，一個(gè)表達(dá)式的意義是在該解釋下的一個(gè)真值指派。2.2.2謂詞演算的語(yǔ)義謂詞演算表達(dá)式的真值設(shè)有表達(dá)式E和在非空論域D上對(duì)E的一個(gè)解釋I，E的真值按以下規(guī)律決定：1）一個(gè)常元的值是根據(jù)I指派給它的D的一個(gè)元素。2）一個(gè)變?cè)闹凳歉鶕?jù)I指派給它的D的一個(gè)元素集合。3）一個(gè)函詞的值是根據(jù)由I指派給它的參數(shù)值計(jì)算得到的D的元素。4）真值符號(hào)true的值是T，false的值是F。5）原子命題的值或者為T，或者為F，取決于解釋I。6）如果一個(gè)命題的值為F，則其否定式為T，否則為F。7）如果…11)如果對(duì)于在解釋I下的X的每一個(gè)指派，S的值為T，則

XS為T，否則為F。12）如果在解釋I下存在X的一個(gè)指派使得S的值為T，則彐XS為T，否則為F。2.2.2謂詞演算的語(yǔ)義(P34)

變?cè)簂ikes(george,X)

這個(gè)變?cè)梢杂扇魏纹渌冊(cè)妫粫?huì)改變表達(dá)式的意思。變?cè)牧吭~約束是謂詞演算語(yǔ)義的重要部分在謂詞演算中,變?cè)袃煞N約束使用的方法:在特定解釋下,命題對(duì)變?cè)淖冇蛑械乃谐Ｔ概蔀檎?則稱該變?cè)侨Q性變?cè)４砣Q量詞的符號(hào)是

,括號(hào)常常用于表示量詞的約束范圍

存在性變?cè)?。至少存在變?cè)淖冇蛑械囊粋€(gè)值使包含變?cè)谋磉_(dá)式為真時(shí)，表達(dá)式才為真。代表存在量詞的符號(hào)是彐2.2.2謂詞演算的語(yǔ)義否定與全稱量詞、存在量詞之間的關(guān)系(P36)。對(duì)于謂詞P,Q,變?cè)猉,Y有：

~彐XP(X)＝X~P(X)~XP(X)＝彐X~P(X)

彐XP(X)＝彐YP(Y)

XQ(X)＝Y(jié)Q(Y)

X(P(X)∧Q(X))＝XP(X)∧YQ(Y)

彐X(P(X)∨Q(X))＝彐XP(X)∨彐YQ(Y)2.3推理規(guī)則產(chǎn)生謂詞演算表達(dá)式2.3.1推理規(guī)則(p38)實(shí)際上是一個(gè)從其他謂詞演算命題產(chǎn)生新的謂詞演算命題的機(jī)械方法。產(chǎn)生基于給定邏輯斷言的句法形式的新命題。當(dāng)每個(gè)由邏輯表達(dá)式集S上的推理規(guī)則產(chǎn)生的命題X都是S的邏輯結(jié)果,則稱該邏輯規(guī)則是合理的。S:xhuman(x)=>mortal(x).human(Socrates).x:mortal(Socrates).假言推理和歸結(jié)原理都是合理的推理規(guī)則的例子。假言推理：如果命題P，P=>Q為真，應(yīng)用假言推理得出Q為真。S:xhuman(x)=>mortal(x).human(Socrates).x:mortal(Socrates).human(Socrates)=>mortal(Socrates)？human(x)

Socrates合一算法2.3.2合一（p40)是判斷兩個(gè)謂詞表達(dá)式匹配所需的一種代入算法合一表明了兩個(gè)或多個(gè)表達(dá)式在什么條件下可以稱為等價(jià)的。替換：一個(gè)替換(Substitution)就是形如{t1/x1,t2/x2,….tn/xn}的有限集合，x1,x2.,,,xn是互不相同的個(gè)體變?cè)?，ti不同于xi,xi也不循環(huán)出現(xiàn)在tj中如：{a/x,g(y)/y,f(g(b))/z}{g(y)/x,f(x)/y}√x合一：設(shè)S={F1，F(xiàn)2，。。。，F(xiàn)n}是一個(gè)原子謂詞公式集合，若存在一個(gè)替換θ，可使F1θ=F2θ=Fnθ,則稱θ為S的一個(gè)合一（Unifier），稱S為可合一的偽代碼寫的函數(shù)Unify

用于計(jì)算兩個(gè)謂詞表達(dá)式的最一般合一以兩個(gè)謂詞演算表達(dá)式為參數(shù),若這兩個(gè)表達(dá)式可以合一,則返回最一般合一代入,否則返回FAIL。2.3.2合一(p42)functionunify(E1,E2);begincase…end%endcaseend首先,它遞歸地試圖對(duì)表達(dá)式的初始成分合一。如果成功,這次合一返回的任何代入式被用到兩個(gè)表達(dá)式的剩下部分,然后以這兩個(gè)表達(dá)式為參數(shù)。終止條件是兩個(gè)參數(shù)之一為一個(gè)符號(hào)(謂詞名,函詞名,變?cè)?常元),或兩個(gè)表達(dá)式的每一元素都已匹配了。2.3.2合一caseE1,E2或者是常元或者是空表:%遞歸終止。IfE1＝E2thenreturn{}elsereturnFAIL;E1是一個(gè)變?cè)?ifE1在E2中出現(xiàn)

thenreturnFAILelsereturn{E2/E1};E2是一個(gè)變?cè)?ifE2在E1中出現(xiàn)

thenreturnFAILelsereturn{E1/E2};

其他情況:%E1和E2都是表2.3.2合一beginHE1:=E1的第一個(gè)元素;HE2:=E2的第一個(gè)元素;SUBS1:=unify(HE1,HE2);ifSUBS1＝FAILthenreturnFAILTE1:=apply(SUBS1,E1的后半部)TE2:=apply(SUBS1,E2的后半部)SUBS2:=unify(TE1,TE2),ifSUBS2＝FAILthenreturnFAILelsereturnSUBS1與SUBS2的合成

end2.3.3合一的一個(gè)例子(p43)通過(guò)以下調(diào)用來(lái)跟蹤算法的運(yùn)行過(guò)程：

unify((parentsX(fatherX)(motherbill)),(parentsbill(fatherbill)Y))

第一次調(diào)用:unify(parents,parents)

這次調(diào)用成功,返回代入集{}。第二次調(diào)用:unify(X,bill)

這次調(diào)用成功,返回代入{bill/X}。2.3.3合一的一個(gè)例子在此基礎(chǔ)上又調(diào)用:unify(((fatherbill)(motherbill)),((fatherbill)Y))

導(dǎo)致調(diào)用:(1)unify((fatherbill),(fatherbill))unify(father,father)unify(bill,bill)unify((),())

所有的調(diào)用都成功,返回空代入集{}。(2)unify((motherbill),Y){bill/X,(motherbill)/Y}2.4應(yīng)用(p46):一個(gè)基于邏輯的金融投資輔助決策程序

一位有三個(gè)人需贍養(yǎng),有$22000存款,每年有$25000的穩(wěn)定收入的投資者的情況,可產(chǎn)生一個(gè)由下列命題組成的邏輯系統(tǒng):1.savings(inadequate)=>investment(savings).2.savings(adequate)∧income(adequate)=>investment(stocks).3.savings(adequate)∧income(inadequate)=>investment(combination).4.Xamountsaved(X)∧彐Y(dependents(Y)∧greater(X,minsavings(Y)))=>savings(adequate).5.Xamountsaved(X)∧彐Y(dependents(Y)∧~greater(X,minsavings(Y)))=>savings(inadequate).2.4應(yīng)用(p47)6.Xearnings(X,steady)∧彐Y(dependents(Y)∧greater(X,minincome(Y)))=>income(adequate).7.Xearnings(X,steady)∧彐Y(dependents(Y)∧~greater(X,minincome(Y)))=>income(inadequate).8.Xearnings(X,unsteady)=>income(inadequate).9.amountsaved(22000).10.earnings(25000,steady).11.dependents(3).其中:minsavings(X)=5000*X;minincome(X)=15000+(4000*X)2.4應(yīng)用(p47)第一步把第10、11與第7的前提合一,得:第二步把第9、11與第4的前提合一,得:13.savings(adequate)3.savings(adequate)∧income(inadequate)=>investment(combination).結(jié)論:investment(combination),這就是給投資者的建議。(存款的人應(yīng)該把他們多余的錢分別用于存款和買股票，在增加存款做保險(xiǎn)的同時(shí)試圖通過(guò)做股票以增加收入。)

12.Income(inadequate).

10.earnings(25000,steady).11.dependents(3).7.Xearnings(X,steady)∧彐Y(dependents(Y)∧~greater(X,minincome(Y)))=>income(inadequate).9.amountsaved(22000).11.dependents(3).4.Xamountsaved(X)∧彐Y(dependents(Y)∧greater(X,minsavings(Y)))=>savings(adequate).AssignmentP62.7對(duì)以下每對(duì)表達(dá)式合一，如果成功，給出最一般合一式1P(X,Y),P(a,Z)2P(X,X),P(a,b)3ancestor(X,Y),ancestor(bill,father(bill))4ancestor(X,father),ancestor(david,george)5g(X),–g(a)6P(X,a,Y),P(Z,Z,b)P62.9*用高級(jí)語(yǔ)言實(shí)現(xiàn)合一算法（思考題）2.5消解定理證明(p48)消解是一種應(yīng)用于謂詞演算中的定理證明技術(shù)，是人工智能問(wèn)題求解的一個(gè)組成部分。消解描述了如何用最少的合一次數(shù)在一個(gè)子句數(shù)據(jù)庫(kù)中發(fā)現(xiàn)矛盾的方法。具體方法如下：對(duì)所要證明的命題取反，把它加到已知為真的公理集中，然后用消解推理規(guī)則證明這將導(dǎo)致一個(gè)矛盾，一旦證明了否定目標(biāo)與已知公理集不一致，就能推導(dǎo)出原來(lái)的目標(biāo)與已知公理集是一致的，從而定理得證。2.5消解定理證明(p48)2.5.1引言消解否證包含以下步驟：把前提或公理轉(zhuǎn)換成子句形式。把求證目標(biāo)的否定的子句形式加到公理集合中。對(duì)所有這些子句進(jìn)行消解，產(chǎn)生它們的邏輯結(jié)果子句。用產(chǎn)生空子句的方法來(lái)得出矛盾。否定目標(biāo)的否證在用于產(chǎn)生空子句的代換下為真。2.5.1引言

消解否證需要所有公理和否定目標(biāo)為子句形式

子句形式把一個(gè)邏輯數(shù)據(jù)庫(kù)表示為一個(gè)文字析取式的集合。一個(gè)文字是一個(gè)原子表達(dá)式或原子表達(dá)式的否定。消解作用于兩個(gè)子句,其中一個(gè)包含某文字,另一個(gè)包含該文字的否定,如果這些文字包含變?cè)?必須用合一使它們相等。一個(gè)新的子句就此產(chǎn)生了,它包含兩個(gè)子句中所有謂詞的析取,除了該文字和它的否定以外。2.5.1引言

用消解所做的等價(jià)的推理把以下謂詞演算公式變換成子句形式(P49)：謂詞形式子句形式1.Alldogsareanimals

(X)(dog(X)→animal(X))~dog(X)∨animal(X)2.Fidoisadogdog(fido)dog(fido)3.allanimalswilldie(Y)(animal(Y)→die(Y))~animal(Y)∨die(Y)

證明：fidowilldie對(duì)目標(biāo)“取反”：~die(fido)~dog(X)∨animal(X).~animal(Y)∨die(Y).

｛Y/X｝

dog(fido).~dog(Y)∨die(Y).

{fido/Y｝

die(fido).~die(fido).

圖2.6“死狗”問(wèn)題消解證明(P50)2.5.1引言2.5.2為消解否證產(chǎn)生子句形式(P49~52)

本節(jié)提出一個(gè)由一系列變換組成的算法，這些變換可以把任何謂詞演算表達(dá)式歸約為子句形式，在此過(guò)程中保持其真值、一般性和不可滿足性不變。即如果在原謂詞演算表達(dá)式中存在一個(gè)矛盾，則其子句形式中也存在一個(gè)矛盾，變換不犧牲消解否證的完備性。2.5.2為消解否證產(chǎn)生子句形式（P50)設(shè)X,Y,Z,W表示變?cè)?；l,m,n表示常元；a,b,c,d,e表示謂詞名。要?dú)w納為子句的表達(dá)式：1.(X)(［a(X)∧b(X)］→［c(X,l)∧(彐Y)((彐Z)［c(Y，Z)］→d(X,Y))］)∨(X)(e(X))

2.(X)(~[a(X)∧b(X)]∨［c(X，l)∧(彐Y)(~(彐Z)［c(Y,Z)］∨d(X,Y))］)∨(Ｘ）(e(X)）3.(X)(［~a(X)∨~b(X)］∨［c(X,l)∧(彐Y)((Z)［~c(Y,Z)］∨d(X,Y))］)∨(X)(e(X))4.(X)([~a(X)∨~b(X)]∨［c(X,l)∧(彐Y)((Z)［~c(Y,Z)］∨d(X,Y))］)∨(W)(e(W))所有量詞移到最左邊而不改變其次序5.(X)(彐Y)(Z)(W)([~a(X)∨~b(X)］∨[c(X,l)∧[~c(Y,Z)]∨d(X,Y))])∨e(W)前束范式斯柯倫標(biāo)準(zhǔn)化去掉所有的存在量詞2.5.2為消解否證產(chǎn)生子句形式斯柯倫標(biāo)準(zhǔn)化：去掉所有的存在量詞彐Z（foo(Y，Z))foo(Y，k)彐X（dog(X))dog(fido)斯柯倫常元如果謂詞中含有多個(gè)參數(shù)，而彐約束變?cè)诩s束變?cè)募s束范圍內(nèi)，則彐約束變?cè)仨毷悄切┢渌冊(cè)暮瘮?shù)。如：（X）(彐Y)(mother(X,Y))（X）(mother(X,m(X))2.5.2為消解否證產(chǎn)生子句形式6.(X)(Z)(W)([~a(X)∨~b(X)］∨［c(X,l)∧[~c(f(X),Z)]∨d(X,f(X)))］)∨e(W)5.(X)(彐Y)(Z)(W)([~a(X)∨~b(X)］∨[c(X,l)∧[~c(Y,Z)]∨d(X,Y))])∨e(W)斯柯倫標(biāo)準(zhǔn)化后去掉全稱量詞7.(［~a(X)∨~b(X)］∨［c(X,l)∧(~c(f(X),Z)∨d(X,f(X)))］)∨e(W)8.［~a(X)∨~b(X)∨c(X,l)∨e(W)］∧[~a(X)∨~b(X)∨~c(f(X),Z)∨d(X,f(X))∨e(W)］轉(zhuǎn)換成析取式的合取每個(gè)合取式為一個(gè)分離的子句9a:~a(X)∨~b(X)∨c(X,l)∨e(W)9b:~a(X)∨~b(X)∨~c(f(X),Z)∨d(X,f(X))∨e(W)重新命名所有變?cè)?，避免重?0a:~a(X)∨~b(X)∨c(X,l)∨e(W)10b:~a(U)∨~b(U)∨~c(f(U),Z)∨d(U,f(U))∨e(V)將公理轉(zhuǎn)換成子句形式：消去蘊(yùn)涵把否定式降至原子公式消去存在量詞如果需要，重新命名變?cè)讶Q量詞移到左邊將析取降至文字式消去合取如果需要，重新命名變?cè)獂[Brick(x)→(彐y[On(x,y)∧Pyramid(y)]∧~彐y[On(x,y)∧On(y,x)]∧

x[~Brick(y)→

~Equal(x,y)])]Homework2.5.3消解證明過(guò)程例1:“幸運(yùn)學(xué)生”的故事（P54):“任何通過(guò)了歷史考試并中了彩票的人是快樂(lè)的。任何肯學(xué)習(xí)或幸運(yùn)的人可以通過(guò)所有考試,John不學(xué)習(xí)但很幸運(yùn),任何人只要是幸運(yùn)的就能中彩。John快樂(lè)嗎?"1.第一步把這些句子變成謂詞形式:定義一些謂詞：pass(x,y),win(x,lottery),happy(x),study(x),lucky(x)2.5.3消解證明過(guò)程“任何通過(guò)了歷史考試并中了彩票的人是快樂(lè)的。任何肯學(xué)習(xí)或幸運(yùn)的人可以通過(guò)所有考試,John不學(xué)習(xí)但很幸運(yùn),任何人只要是幸運(yùn)的就能中彩。John快樂(lè)嗎?"X(pass(X,history)∧win(X,lottery)→happy(X))

XY(study(X)∨lucky(X)→pass(X,Y))~study(john)∧lucky(john)

X(lucky(X)→win(X,lottery))2.5.3消解證明過(guò)程1.~pass(X,history)∨~win(X,lottery)∨happy(X)2.~study(Y)∨pass(Y,Z)3.~lucky(V)∨pass(V,W)4.~study(john)5.lucky(john)6.~lucky(U)∨win(U,lottery)X(pass(X,history)∧win(X,lottery)→happy(X))

XY(study(X)∨lucky(X)→pass(X,Y))~study(john)∧lucky(john)

X(lucky(X)→win(X,lottery))將這四個(gè)謂詞演算命題轉(zhuǎn)換成子句形式:加入子句形式的否定目標(biāo):7.~happy(john)2.5.3消解證明過(guò)程~pass(X,history)∨

win(U,lottery)∨~lucky(U)~win(X,lottery)∨happy(X)

｛U/X｝

~pass(U,history)∨

~happy(john).happy(U)∨~lucky(U).

｛john/U｝

lucky(john).

~pass(john,history)∨~lucky(john).

~pass(john,history).

~lucky(∨)∨pass(V,W).

｛john/V,history/W｝

lucky(john).

~lucky(john).

圖2.8“快樂(lè)學(xué)生”問(wèn)題的消解否證*將(P55)C改為U子句1子句6子句7子句5子句3子句5John是快樂(lè)的2.5.3消解證明過(guò)程例2：(P54)假設(shè):

“所有不貧窮并且聰明的人是快樂(lè)的。那些看書的人是不笨的。John能看書并且富有?？鞓?lè)的人過(guò)著激動(dòng)人心的生活。你能發(fā)現(xiàn)誰(shuí)過(guò)著激動(dòng)人心的生活嗎?"把上述故事翻譯成謂詞演算表達(dá)式:X((~poor(X)∧smart(X))→happy(X)Y(read(Y)→smart(Y))read(john)∧~poor(john)Z(happy(Z)→exciting(Z))否定目標(biāo)是：~

彐W(exciting(W))

2.5.3消解證明過(guò)程1.poor(X)∨~smart(X)∨happy(X)2.~read(Y)∨smart(Y)3.read(john)4.~poor(john)5.~happy(Z)∨exciting(Z)6.~exciting(W)X((~poor(X)∧smart(X))→happy(X)Y(read(Y)→smart(Y))read(john)∧~poor(john)Z(happy(Z)→exciting(Z))~

彐W(exciting(W))

變換成如下的子句:2.5.3消解證明過(guò)程~exciting(W)~happy(Z)∨exciting(Z)

｛Z/W｝

~happy(Z)poor(X)∨~smart(X)∨happy(X)

｛X/Z｝

poor(X)∨~smart(X)~read(Y)∨smart(Y)

｛Y/X｝

poor(Y)∨~read(Y)~poor(john)子句6子句5子句1子句2這個(gè)例子的消解否證如圖2.9(P56)所示：

｛john/Y｝~read(john)read(john)子句4子句3從消解否證中提取答案2.6用消解法求更為復(fù)雜問(wèn)題例子例1：某記者到一孤島采訪，遇到了一個(gè)難題，即島上有許多人說(shuō)假話，因而難以保證新聞報(bào)道的正確性，不過(guò)有一點(diǎn)他是清楚的，這個(gè)島上的人有一特點(diǎn)：說(shuō)假話的人從來(lái)不說(shuō)真話，說(shuō)真話的人也從來(lái)不說(shuō)假話。一次記者遇到了孤島上的三個(gè)人，為了弄清楚誰(shuí)說(shuō)真話，誰(shuí)說(shuō)假話，他向這三個(gè)人中的每一個(gè)都問(wèn)了一個(gè)同樣的問(wèn)題，即“誰(shuí)是說(shuō)謊者？”

結(jié)果A答“B和C都是說(shuō)謊者”，

B答“A和C都是說(shuō)謊者”，

C答“A和B中至少有一個(gè)是說(shuō)謊者”，試問(wèn)記者如何從回答中理出頭緒。2.6用消解法求更為復(fù)雜問(wèn)題例子以A，B，C三個(gè)命題來(lái)表示A，B，C三個(gè)是老實(shí)人（不說(shuō)謊）A答“B和C都是說(shuō)謊者”B答“A和C都是說(shuō)謊者”C答“A和B中至少有一個(gè)是說(shuō)謊者”如果A說(shuō)真話，則B和C一定說(shuō)謊，因此有：A→~B∧~C

如果A說(shuō)假話，則B和C中至少有一人說(shuō)真話,因此有:~

A→B∨C以同樣的推理方式可得到：如果B說(shuō)真話,如果B說(shuō)假話

B→~A∧~C~

B→A∨C如果C說(shuō)真話,如果C說(shuō)假話

C→~A∨

~B~

C→A

∧

B2.6用消解法求更為復(fù)雜問(wèn)題例子對(duì)以上蘊(yùn)含式加以推理,并化成子句形式,可得：

~A∨~B（1）

~A∨~C（2）

A∨B∨C（3）

~B∨~C（4）

~A∨~B∨~C（5）

A∨C（6）

B∨C（7）2.6用消解法求更為復(fù)雜問(wèn)題例子（1）和（7）消解，得：~

A∨C（8）（2）和（8）消解，得：~

A

（9）（6）和（9）消解，得：C

（10）（4）和（10）消解，得：~

B

（11）說(shuō)明？誰(shuí)是說(shuō)謊者？A和B都是說(shuō)謊者，而C是老實(shí)人2.6用消解法求更為復(fù)雜問(wèn)題例子