謂詞邏輯二1LuChaojun,SJTU主要內容謂詞與量詞謂詞公式等值演算范式謂詞邏輯推理歸結法推理2LuChaojun,SJTULuChaojun,SJTU3公式的等值謂詞公式A和B如果在任一解釋下都有相同的真值,就說A和B等值(或等價),記作AB.定理 AB

iff

A?B是永真式注:教材上干脆以此定理作為等值的定義.3LuChaojun,SJTU約束變元換名規(guī)則約束變元的名字是無關緊要的.換名規(guī)則:對于公式(x)A(或(x)A),設變元y不在A中出現,將A中所有受此量詞約束的x出現都換成y得到A,且量詞改成(y)(或(y)).得到的公式(y)A(或(y)A)與原公式等值.4LuChaojun,SJTU自由變元替換規(guī)則替換規(guī)則:對于公式A,x在A中出現,y不在A中出現.將A中所有x的自由出現都換成y,得到A,則A與A等值.5LuChaojun,SJTU由PL得到FOL的等值式定義:設A是含命題變元p1,…,pn的命題邏輯公式,A1,…,An是謂詞邏輯公式.對1in,用Ai替換pi的每一處出現,所得謂詞邏輯公式A稱為命題邏輯公式A的替換實例.

定理:命題邏輯的永真式(或永假式)的任何替換實例都是謂詞邏輯的永真式(或永假式).推論:命題邏輯的等值式可經替換得到謂詞邏輯的等值式.例如:pp

(x)P(x)

(x)P(x)pqpq

P(x)Q(x)

P(x)

Q(x)6LuChaojun,SJTU基本等值式(1)量詞的轉化(x)P(x)

(x)P(x)(x)P(x)

(x)P(x)例:(x)(Animal(x)Cat(x))并非動物都是貓(x)(Animal(x)Cat(x))(x)(Animal(x)

Cat(x))存在不是貓的動物7LuChaojun,SJTU基本等值式(2)對,

對的分配律(x)(P(x)Q(x))(x)P(x)(x)Q(x)(x)(P(x)Q(x))(x)P(x)(x)Q(x)對,

對沒有分配律!例如:(x)(Man(x)Woman(x))所有人要么是男人要么是女人.(x)Man(x)(x)Woman(x)要么所有人都是男人,要么所有人都是女人.8LuChaojun,SJTU基本等值式(3)量詞對及的分配律(x)(P(x)B)(x)P(x)B

(x)(P(x)B)(x)P(x)B(x)(P(x)B)(x)P(x)B(x)(P(x)B)(x)P(x)B其中B不含x的自由出現!或干脆規(guī)定B不含x這個條件很容易滿足:對約束變元改名即可.9LuChaojun,SJTU基本等值式(4)量詞對的分配律(x)(P(x)

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

B)(x)P(x)

B

(x)(BP(x))

B(x)P(x)(x)(P(x)B)(x)P(x)B(x)(BP(x))

B(x)P(x)其中B不含x的自由出現!或干脆規(guī)定B不含x10LuChaojun,SJTU基本等值式(5)量詞交換律(x)(y)P(x,y)

(y)(x)P(x,y)(x)(y)P(x,y)

(y)(x)P(x,y)11LuChaojun,SJTU等值演算利用基本等值式,進行謂詞邏輯的推理.判斷永真式例:((x)P(x)(x)Q(x))(x)(P(x)Q(x))……12LuChaojun,SJTULuChaojun,SJTU主要內容謂詞與量詞謂詞公式等值演算范式謂詞邏輯推理歸結法推理13LuChaojun,SJTULuChaojun,SJTU14范式回憶:任何命題邏輯公式都有與之等值的范式.謂詞邏輯公式也有范式前束范式:與原公式等值Skolem范式:與原公式只有較弱的關系(等可滿足性)14LuChaojun,SJTULuChaojun,SJTU15前束范式定義:如果公式A中的所有量詞都非否定地置于公式左端,且其轄域都延伸到公式的末端,則稱A是前束范式(prenexnormalform).即:A形如 (Q1x1)…(Qnxn)M(x1,…,xn)

其中諸Qi為量詞或,M不含量詞,稱為A的母式(基式,matrix).前束范式定理:任一公式都有與之等值的前束范式.15LuChaojun,SJTULuChaojun,SJTU16如何轉化成PNF1.消去和?2.否定詞內移應用DeMorgan律3.約束變元易名(如果必要的話)4.量詞左移應用分配等值式16LuChaojun,SJTULuChaojun,SJTU17例:求PNF((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)))(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))(x)((y)P(a,x,y)

(y)Q(y,b)R(x))(x)((y)P(a,x,y)

(z)Q(z,b)R(x))

(x)(y)(z)(P(a,x,y)

Q(z,b)R(x))(x)(z)(y)(P(a,x,y)

Q(z,b)R(x))(x)(y)(z)(P(a,x,y)Q(z,b)R(x)(pp))1717LuChaojun,SJTULuChaojun,SJTU18Skolem范式前束范式對前束量詞沒有次序要求,也沒有其他要求.如果對前束范式進而要求所有都在之左,或者只保留而消去 便得Skolem范式的兩種形式.18LuChaojun,SJTULuChaojun,SJTU19Skolem范式(1):-前束范式一個公式的-前束范式形如(x1)…(xi)(xi+1)…(xn)M(x1,…,xn)是前束范式至少有一個存在量詞存在量詞都在全稱量詞的左邊M(x1,…,xn)中不再有量詞,也無自由個體變元19LuChaojun,SJTULuChaojun,SJTU20-前束范式定理定理:任一公式A都可化為-前束范式A,并且 A普遍有效iff

A普遍有效.說明:只有普遍有效的公式A,才與其-前束范式是等值的.一般的公式與其-前束范式并不等值.用于FOL完備性的證明.20LuChaojun,SJTULuChaojun,SJTU21例:-前束范式求(x)(y)(u)P(x,y,u)的-前束范式(P中無量詞).1.先求前束范式.本例已是.2.關鍵一步:(y)改寫成(y)...(z).形如 (x)((y)(u)(P(x,y,u)

S(x,y))(z)S(x,z))引入新謂詞S和新變元z.(直觀意義?)3.(z)左移即得結果:

(x)(y)(u)(z)((P(x,y,u)

S(x,y))S(x,z))當有多個在的左邊,可按此法逐一右移.21LuChaojun,SJTULuChaojun,SJTU22Skolem范式(2):無前束范式PNF中消去所有而只保留.術語“Skolem范式”一般指這種形式.定理:任一公式A都可化為Skolem范式A,并且 A(不)可滿足iff

A(不)可滿足.不是等值(equivalent),而是“等可滿足”(equisatisfiable).22LuChaojun,SJTULuChaojun,SJTU23例:Skolem范式(x)(y)(z)(u)(v)(w)P(x,y,z,u,v,w)1.先求前束范式.本例已是.2.關鍵:消去.方法是引入個體常元或函數.如 (y)(z)(u)(v)(w)P(a,y,z,u,v,w)消去x:引入新個體常元a代入x3.消去(u)時,引進的個體因為與左邊的y和z有關,所以不能用個體常項,而是用函數

(y)(z)(v)(w)P(a,y,z,f(y,z),v,w)4.消去(w):(y)(z)(v)P(a,y,z,f(y,z),v,g(y,z,v))23LuChaojun,SJTULuChaojun,SJTU24例:Skolem范式不保持等值比較(x)(y)P(x,y)與(x)P(x,f(x)):在{1,2}域上 (x)(y)P(x,y)

(P(1,1)

P(1,2))

(P(2,1)P(2,2)) (x)P(x,f(x))

P(1,f(1))

P(2,f(2))兩者明顯不等值.但在(不)可滿足的意義下兩者是一致的.24LuChaojun,SJTULuChaojun,SJTU主要內容謂詞與量詞謂詞公式等值演算范式謂詞邏輯推理歸結法推理25LuChaojun,SJTULuChaojun,SJTU26謂詞邏輯推理命題邏輯中有關永真蘊涵和推理的形式結構等的討論都可引伸到謂詞邏輯中,并可把命題邏輯推理作為謂詞邏輯推理的一個部分.這里我們討論謂詞邏輯所特有的推理形式和基本推理公式.26LuChaojun,SJTULuChaojun,SJTU27回顧:永真蘊涵關系給定公式A和B,若在任何賦值下,A為真則B也為真,則稱A永真蘊涵B,記作AB.A是前提,

B是A的邏輯結論.即日常所說的“推出”關系2727LuChaojun,SJTU與的關系定理:對公式A和B, AB

iff

AB是永真式所以A

B

稱為永真蘊涵式.注:教材中干脆利用來定義.定理:對公式A和B, AB

iff

A

B是矛盾式LuChaojun,SJTU2828LuChaojun,SJTULuChaojun,SJTU29基本永真蘊涵式(I14)(x)P(x)(x)Q(x)(x)(P(x)

Q(x))(I15)(x)(P(x)

Q(x))(x)P(x)(x)Q(x)(I16)(x)P(x)(x)Q(x)(x)(P(x)

Q(x))(I17)(x)P(x)(x)P(x)(I18)(x)(y)P(x,y)(y)(x)P(x,y)(I21)(x)(y)P(x,y)(y)(x)P(x,y)

(x)(P(x)

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

(x)(P(x)

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

(x)(P(x)

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

(x)(P(x)

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

(x)(P(x)Q(x))(x)(Q(x)R(x))(x)(P(x)R(x))

(x)(P(x)

Q(x))

P(a)

Q(a)29LuChaojun,SJTULuChaojun,SJTU30舉例說明:基本永真蘊涵式(I15)(x)(P(x)

Q(x))(x)P(x)(x)Q(x)語義說明:若個體域是某班學生,P(x)表示x是高材生,Q(x)表示x是運動健將,那么(x)(P(x)Q(x))表示有學生既是高材生又是運動健將,而(x)P(x)(x)Q(x)是說有高材生并且有運動健將(但不要求高材生和運動健將是同一個學生). 顯然成立,因為結論比前提弱.但此推理的逆不成立.30LuChaojun,SJTULuChaojun,SJTU31推理規(guī)則命題邏輯中的推理演算可推廣到謂詞邏輯.推理規(guī)則(P規(guī)則,T規(guī)則,CP規(guī)則等)都可直接移入謂詞邏輯.此外,還需引入4條有關量詞的推理規(guī)則.31LuChaojun,SJTULuChaojun,SJTU32全稱特指規(guī)則US(UniversalSpecification): (x)A(x)A(y)y是個體變元,A(y)是在A(x)中對x代入y的結果.左:A對所有個體為真,右:那對任一個體y,A(y)當然為真.特例:用個體常元代入x..要確保引入的y的任意性(即自由變元),因此:當A(x)中含有量詞和其他變元時,需使得y不被量詞約束.例如:(x)((z)(x<z))在實數上成立,于是(z)(y<z)也成立.但若將y取為z,便有(z)(z<z),這是矛盾式.32LuChaojun,SJTULuChaojun,SJTU33存在特指規(guī)則ES(ExistentialSpecification): (x)A(x)A(c)含義:如果存在個體使A(x)為真,那么就讓c是這種個體,則A(c)當然為真.c不能在A(x)中,前面的推導中,及待證結論中出現.反例:在實數域上(x)(c<x)是成立的,但c<c不成立.還需限制(x)A(x)中沒有自由個體變元出現.反例:實數域上(x)(x>y)成立.由于y是自由個體變元,這時不能推導出c>y.這時可引入個體函數c(y).這是數學里常用的存在推理法.33LuChaojun,SJTULuChaojun,SJTU34全稱推廣規(guī)則UG(UniversalGeneralization):

A(y)(x)A(x).若任意個體y(自由變元)都使A為真,則(x)A(x)為真.限制:x不在A(y)中出現.使引入的量詞不能約束A中其他變元為確保y的任意性,在獲得A(y)的推導過程中:y可通過US,條件證明或歸謬證明的假設引入各前提中y不是自由變元;未使用過ES規(guī)則,或未使用ES引入y,或未使用ES引入z(y)例:(z)(z>y)在實數域上成立,則(x)((z)(z>x))也成立.但若引入(z),(z)(z)(z>z)是不成立的.又:若前面引入的y代表某特定個體,也不能作UG34LuChaojun,SJTULuChaojun,SJTU35存在推廣規(guī)則EG(ExistentialGeneralization): A(c)(x)A(x)含義:如果有個體常項c使A為真,那么(x)A(x)為真.其中c是個體常項.需限制x不出現在A(c)中.反例:實數域上(x)(x>0)成立,但(x)(x)(x>x)不成立.35LuChaojun,SJTULuChaojun,SJTU36多個量詞下的規(guī)則使用(x)(y)A(x,y)(y)A(x,y)右端不能寫成(y)A(y,y)(x)A(x,c)(y)(x)A(x,y)右端不能寫成(x)(x)A(x,x)(x)(y)A(x,y)(y)A(x,y)A(x,c)但不能反推出(x)A(x,c)和(y)(x)A(x,y)!原因是(x)(y)A(x,y)成立時,對每個x所找到的y是依賴于x的,從而A(x,y)的成立是有條件的,不是對所有的x都有同一個y.36LuChaojun,SJTULuChaojun,SJTU37推理演算在謂詞邏輯里,要證明AB,真值表法不適用,又不存在判明A→B普遍有效的一般方法.從而使用推理規(guī)則的推理演算是謂詞邏輯的基本推理方法.推理演算過程:首先將以自然語句表示的推理問題形式化表示若不能直接使用基本永真蘊涵式,便消去量詞,在無量詞下使用規(guī)則和公式推理最后再引入量詞．37LuChaojun,SJTULuChaojun,SJTU38例:推理演算(1)前提:(x)(P(x)→Q(x)),(x)(Q(x)→R(x))結論:(x)(P(x)→R(x))證明

(1)(x)(P(x)→Q(x)) P(前提)

(2)P(x)→Q(x) US

(3)(x)(Q(x)→R(x)) P

(4)Q(x)→R(x) US

(5)P(x)→R(x) T(2),(4)I10

(6)(x)(P(x)→R(x)) UG38LuChaojun,SJTULuChaojun,SJTU39例:推理演算(2)人皆有死,蘇格拉底是人,所以蘇格拉底會死.令P(x):x是人,Q(x):x會死.于是問題可改述為 (x)(P(x)→Q(x))P(Socrates)→Q(Socrates)證明

(1)(x)(P(x)→Q(x)) P

(2)P(x)→Q(x) US

(3)P(Socrates)→Q(Socrates) 替換 (4)P(Socrates) P

(4)Q(Socrates) T(3)(4)I1039LuChaojun,SJTULuChaojun,SJTU40例:推理演算(3)前提:(x)P(x)→(x)((P(x)Q(x))→R(x)),(x)P(x)結論:(x)(y)(R(x)R(y))證明

(1)(x)P(x)→(x)((P(x)Q(x))→R(x))P

(2)(x)P(x) P

(3)(x)((P(x)Q(x))→R(x)) T(1)(2)I10

(4)P(c) (2)

ES

(5)(P(x)Q(x))→R(x) (3)US(6)

(P(c)Q(c))→R(c) 替換(7)P(c)Q(c) T(4)I3(8)R(c) T(6)(7)I10

(9)(x)R(x) (8)

EG

(10)(y)R(y) (8)

EG

(11)(x)R(x)(y)R(y) (9)(10)(12)(x)(y)(R(x)R(y)) (11)E3840LuChaojun,SJTULuChaojun,SJTU41例:推理演算(4)分析下面推理的正確性.

(1)(x)(y)(x>y) P

(2)(y)(z>y) US

(3)z>b ES

(4)(z)(z>b) UG

(5)b>b US

(6)(x)(x>x) UG從(1)到(2),應記住y是依賴于z的.從(2)到(3),b是依賴于z的.從(3)到(4)不成立:因為b是依賴于z的.從(5)到(6)也錯:因為b是常項.41LuChaojun,SJTULuChaojun,SJTU主要內容謂詞與量詞謂詞公式等值演算范式謂詞邏輯推理歸結法推理42LuChaojun,SJTULuChaojun,SJTU43謂詞邏輯的歸結推理法歸結證明法可推廣到謂詞邏輯,證明過程同命題邏輯,只不過要考慮量詞和個體變元帶來的復雜性.使用推理規(guī)則的推理演算靈活而技巧性強;歸結法較為機械,易于計算機實現.43LuChaojun,SJTU歸結證明過程1.寫出G=AB回憶:為證明AB,可等價地證明AB不可滿足.2.建立G的子句集S將G化成等值的前束范式;再化成無前束范式(母式合取范式化)G*;回憶:G不可滿足iff

G*不可滿足再將G*中的省略,并將G*中的每個簡單析取式表示為一個子句,便得子句集S.S中的變元均被約束S與G是同不可滿足的44LuChaojun,SJTU歸結證明過程(續(xù))3.對S進行一步歸結:

若S中有兩個子句C1=L1C1,C2=L2C