第四章自動推理

第四章自動推理第一頁，共一百二十四頁，2022年，8月28日自動推理第二頁，共一百二十四頁，2022年，8月28日自動推理的理論和技術(shù)是專家系統(tǒng)、程序推導(dǎo)、程序正確性證明、智能機器人等研究領(lǐng)域的重要基礎(chǔ)。自動推理早期的工作主要集中在機器定理證明。1930年Herbrand為定理證明建立了一種重要方法，他的方法奠定了機械定理證明的基礎(chǔ)。機械定理證明的主要突破是1965年由做出的，他建立了所謂歸結(jié)原理，使機械定理證明達到了應(yīng)用階段。第三頁，共一百二十四頁，2022年，8月28日Agenda引言命題邏輯中的歸結(jié)原理謂詞邏輯中的歸結(jié)原理非單調(diào)推理第四頁，共一百二十四頁，2022年，8月28日引言（1）從一個或幾個已知的判斷(前提)邏輯地推論出一個新的判斷(結(jié)論)的思維形式稱為推理,這是事物的客觀聯(lián)系在意識中的反映。自動推理早期的工作主要集中在機器定理證明。機械定理證明的中心問題是尋找判定公式是否是有效的（或是不一致的）通用程序。若按推理過程中推出的結(jié)論是否單調(diào)地增加，或者說推出的結(jié)論是否越來越接近最終目標(biāo)來劃分，推理可以分為單調(diào)推理和非單調(diào)推理。第五頁，共一百二十四頁，2022年，8月28日引言（2）所謂單調(diào)推理是指在推理過程中隨著推理的向前推進以及新知識的加入，推出的結(jié)論呈單調(diào)增加的趨勢，并且越來越接近最終目標(biāo)，在推理過程中不會出現(xiàn)反復(fù)的情況，即不會由于新知識的加入否定了前面推出的結(jié)論，從而使推理又退回到前面的某一步。所謂非單調(diào)推理是指在推理過程中由于新知識的加入，不僅沒有加強已推出的結(jié)論，反而要否定它，使得推理退回到前面的某一步，重新開始。非單調(diào)推理是在知識不完全的的情況下發(fā)生的。第六頁，共一百二十四頁，2022年，8月28日引言（3）在現(xiàn)實世界中存在大量不確定問題。不確定性來自人類的主觀認識與客觀實際之間存在差異。事物發(fā)生的隨機性,人類知識的不完全、不可靠、不精確和不一致,自然語言中存在的模糊性和歧義性都反映了這種差異,都會帶來不確定性。針對不同的不確定性的起因,人們提出了不同的理論和推理方法。在下章中，我們將對不確定性推理進行討論。第七頁，共一百二十四頁，2022年，8月28日引言（4）證明的基本思想是：設(shè)F1、…、Fn、G為公式，G為F1、…、Fn的邏輯推論，當(dāng)且僅當(dāng)公式（（F1…Fn）G）是有效的

也可以采用反證法的思想：設(shè)F1、…、Fn、G為公式，G為F1、…、Fn的邏輯推論，當(dāng)且僅當(dāng)公式（F1…Fn

G）是不可滿足的

歸結(jié)法的本質(zhì)上就是一種反證法，它是在歸結(jié)推理規(guī)則的基礎(chǔ)上實現(xiàn)的：為了證明一個命題P恒真，它證明其反命題～P恒假，即不存在使得P為真的解釋

第八頁，共一百二十四頁，2022年，8月28日Agenda引言命題邏輯中的歸結(jié)原理謂詞邏輯中的歸結(jié)原理非單調(diào)推理第九頁，共一百二十四頁，2022年，8月28日命題邏輯中的歸結(jié)原理子句和子句形歸結(jié)

歸結(jié)反演合理性和完備性歸結(jié)反演的搜索策略第十頁，共一百二十四頁，2022年，8月28日子句和子句形（1）文字是原子或其否定子句是文字的析取完備連接符集合：合取范式（CNF）（L11…L1n1)…(Lm1…Lmnm)析取范式（DNF）（L11…L1n1)…(Lm1…Lmnm)定理：對任意公式，都有與之等值的合取范式和析取范式轉(zhuǎn)換方法：一般方法真值表方法第十一頁，共一百二十四頁，2022年，8月28日子句和子句形（2）一般方法EliminateimplicationsignsbyusingtheequivalentformusingReducethescopesof~signsbyusingDeMorgan’slawandbyeliminatingdouble~signsConverttoCNFbyusingtheassociativeanddistributivelaws.第十二頁，共一百二十四頁，2022年，8月28日Resolution

對任意三個文字p、q和rpr,q~rpq

或者：forC1=PC1’,C2=~PC2’PC1’,~PC2’C1’C2’歸結(jié)式：R(C1,C2)=C1’C2’證明：第十三頁，共一百二十四頁，2022年，8月28日ResolutionRefutations（1）定理證明的任務(wù):由前提A1A2...An推出結(jié)論B即證明:A1A2...AnB永真轉(zhuǎn)化為證明:A1A2...An~B為永假式歸結(jié)推理就是:從A1A2...An~B出發(fā),使用歸結(jié)推理規(guī)則來找出矛盾,最后證明定理A1A2...AnB的成立第十四頁，共一百二十四頁，2022年，8月28日ResolutionRefutations（2）歸結(jié)方法是一種機械化的,可在計算機上加以實現(xiàn)的推理方法可認為是一種反向推理形式提供了一種自動定理證明的方法第十五頁，共一百二十四頁，2022年，8月28日ResolutionRefutations（3）一般過程:建立子句集S從子句集S出發(fā),僅對S的子句間使用歸結(jié)推理規(guī)則如果得出空子句,則結(jié)束;否則轉(zhuǎn)下一步將所得歸結(jié)式仍放入S中對新的子句集使用歸結(jié)推理規(guī)則轉(zhuǎn)(3)空子句不含有文字,它不能被任何解釋滿足,所以空子句是永假的,不可滿足的歸結(jié)過程出現(xiàn)空子句,說明出現(xiàn)互補子句對,說明S中有矛盾,因此S是不可滿足的.第十六頁，共一百二十四頁，2022年，8月28日ResolutionRefutations（4）例子:證明(PQ)~Q~p首先建立子句集:(PQ)~Q~(~P)(~PQ)~QPS={~PQ,~Q,P}對S作歸結(jié):(1)~PQ(2)~Q(3)P(4)~P(1)(2)歸結(jié)(5)(3)(4)歸結(jié)第十七頁，共一百二十四頁，2022年，8月28日SoundnessandCompleteness歸結(jié)原理是合理的歸結(jié)原理是完備的第十八頁，共一百二十四頁，2022年，8月28日ResolutionRefutationSearchStrategies

有序策略（Orderstrategies）Refinementstrategies支持集（Setofsupport）:每次歸結(jié)時，參與歸結(jié)的子句中至少應(yīng)有一個是由目標(biāo)公式的否定所得到的子句，或者是它們的后裔該策略是完備的線性輸入（LinearInput）：參與歸結(jié)的兩個子句中至少有一個是初始子句集中的子句該策略是不完備的祖先過濾（AncestryFiltering）：參與歸結(jié)的兩個子句中至少有一個是初始子句集中的句子，或者是另一個子句的祖先該策略是完備的第十九頁，共一百二十四頁，2022年，8月28日Agenda引言命題邏輯中的歸結(jié)原理謂詞邏輯中的歸結(jié)原理非單調(diào)推理第二十頁，共一百二十四頁，2022年，8月28日謂詞邏輯歸結(jié)方法子句形歸結(jié)原理歸結(jié)的完備性第二十一頁，共一百二十四頁，2022年，8月28日子句形--SKOLEM標(biāo)準型

前束范式

(Q1x1)…(Qnxn)M(x1,…,xn)前束形==(前綴){母式}量詞串無量詞公式定理：任何公式G都等價于一個前束范式Skolem函數(shù)：存在量詞不出現(xiàn)在全稱量詞的轄域內(nèi),此時只要用一個新的個體常量(稱為Skolem常量)替換受該存在量詞約束的變元就可消去存在量詞存在量詞位于一個或多個全稱量詞的轄域內(nèi).此時需要Skolem函數(shù),該函數(shù)的變元就是由那些全稱量詞所約束的全稱量詞量化的變量.Skolem函數(shù)所使用的函數(shù)符號必須是新的.第二十二頁，共一百二十四頁，2022年，8月28日子句形--SKOLEM標(biāo)準型Skolem標(biāo)準型：沒有存在量詞的公式。設(shè)G是一階邏輯中的公式，將其化為Skolem標(biāo)準型，母式M給出的子句集S稱為公式G的子句集第二十三頁，共一百二十四頁，2022年，8月28日子句形—化子句集-1謂詞公式化為子句形的步驟x[P(x)[y[P(y)P(f(x,y))]~y[Q(x,y)P(y)]]](1)消去蘊含符號:PQ~PQx[~P(x)[y[~P(y)P(f(x,y))]~y[~Q(x,y)P(y)]]](2)減少否定符號的轄域,把“~”移到緊靠謂詞的位置上~(~P)P~(PQ)~P~Q~(PQ)~P~Q~(x)P(x)~P~(x)P(x)~Px[~P(x)[y[~P(y)P(f(x,y))]y[Q(x,y)~P(y)]]]第二十四頁，共一百二十四頁，2022年，8月28日子句形—化子句集-2(3)變量標(biāo)準化:重新命名變元名,使不同量詞約束的變元有不同的名字.x[~P(x)[y[~P(y)P(f(x,y))]w[Q(x,w)~P(w)]]](4)消去存在量詞:x[~P(x)[y[~P(y)P(f(x,y))][Q(x,g(x))~P(g(x))]]]第二十五頁，共一百二十四頁，2022年，8月28日子句形—化子句集-3(5)化為前束形:把所有的全稱量詞移到公式的左邊,并使每個量詞的轄域包含這個量詞后面公式的整個部分.即得前束形上例變?yōu)?xy[~P(x)[[~P(y)P(f(x,y))][Q(x,g(x))~P(g(x))]]](6)把母式化為合取范式:上例變?yōu)?xy[[~P(x)~P(y)P(f(x,y))] [~P(x)Q(x,g(x))] [~P(x)~P(g(x))]]第二十六頁，共一百二十四頁，2022年，8月28日子句形—化子句集-4(7)消去全稱量詞:[[~P(x)~P(y)P(f(x,y))][~P(x)Q(x,g(x))][~P(x)~P(g(x))]](8)消去連結(jié)詞符號~P(x)~P(y)P(f(x,y))~P(x)Q(x,g(x))~P(x)~P(g(x))(9)更換變量名稱:對變元更名,使不同子句中的變元不同名.~P(x1)~P(y)P(f(x1,y))~P(x2)Q(x2,g(x2))~P(x3)~P(g(x3))第二十七頁，共一百二十四頁，2022年，8月28日子句形—化子句集--6一個子句內(nèi)的文字可含有變量,但這些變量總是被理解為全稱量詞量化的變量G與其子句集S并不等值.但是在不可滿足的意義下兩者是等價的.而且G是S的邏輯推論,SG.反過來不成立第二十八頁，共一百二十四頁，2022年，8月28日謂詞邏輯的子句形--定理定理:若G是給定的公式,而相應(yīng)的子句集為S,則G是不可滿足的當(dāng)且僅當(dāng)S是不可滿足的推論：設(shè)G=G1…Gn,Si

是Gi的Skolem標(biāo)準型，令S=Si…Sn，則，G是不可滿足的當(dāng)且僅當(dāng)S是不可滿足的。第二十九頁，共一百二十四頁，2022年，8月28日示例-1例1:證明梯形的對角線與上下底構(gòu)成的內(nèi)錯角相等設(shè)給定梯形的頂點依次為:a,b,c,d.T(x,y,u,v):表示以xy為上底,uv為下底的梯形P(x,y,u,v):表示xy平行于uvE(x,y,z,u,v,w):表示xyz=uvw問題的邏輯描述和相應(yīng)的子句集為:A1:(x)(y)(u)(v)(T(x,y,u,v)P(x,y,u,v))SA1:~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))SA2:~P(x,y,u,v)E(x,y,v,u,v,y)第三十頁，共一百二十四頁，2022年，8月28日示例-1(續(xù)）A3:T(a,b,c,d)(已知)SA3:T(a,b,c,d)B:E(a,b,d,c,d,b)(要證的結(jié)論)S~B:~E(a,b,d,c,d,b)因此:S=SA1SA2

SA3

S~B第三十一頁，共一百二十四頁，2022年，8月28日示例-2例2:對所有的x,y,z來說,如果y是x父親,z是y的父親,則z是x的祖父.又知道每個人都有父親,試問對某個人來說,誰是他的祖父?引入謂詞:P(x,y):表示x是y的父親Q(x,y):表示x是y的祖父A1:(x)(y)(z)(P(x,y)P(y,z)Q(x,z))SA1:~P(x,y)~P(y,z)Q(x,z)A2:(y)(x)P(x,y)SA2:P(f(y),y)第三十二頁，共一百二十四頁，2022年，8月28日示例-2（續(xù)）B:(x)(y)Q(x,y)(要證的結(jié)論)S~B:~Q(x,y)ANS(x)其中ANS(x)是人為增加的,在推理過程中,ANS(x)變量x同Q(x,y)中的x作同樣的變換,當(dāng)推理結(jié)束的時候,ANS(x)中的變量x便給出了問題的解答因此:S=SA1SA2

S~B第三十三頁，共一百二十四頁，2022年，8月28日謂詞邏輯中的歸結(jié)原理置換與合一歸結(jié)式歸結(jié)反演第三十四頁，共一百二十四頁，2022年，8月28日置換(Substitution)（1）例：C1：P(x)Q(x)C2：~P(f(x))R(x)沒有互補對;例：C1：P(y)Q(y){y/x}C1：P(f(x))Q(f(x)){f(x)/y}C3：R(x)

Q(f(x))第三十五頁，共一百二十四頁，2022年，8月28日置換(2）置換和合一是為了處理謂詞邏輯中子句之間的模式匹配而引進.定義:

置換是形如{t1/v1,t2/v2,…,tn/vn}的一個有限集.其中vi是變量,而ti是不同于vi的項(常量,變量,函數(shù)),且vi

vj(ij)

,

i,j=1,…,n例子：{a/x,w/y,f(s)/z},{g(x)/x}是置換;{x/x},{y/f(x)}不是置換;第三十六頁，共一百二十四頁，2022年，8月28日置換-（3）定義：不含任何元素的置換稱為空置換，記為定義:設(shè)={t1/v1,t2/v2,…,tn/vn}是一個置換，E是一個表達式。將E中出現(xiàn)的每一個變量符號vi（1in）,都用項ti置換，這樣得到的表達式記為E，稱E為E的例。第三十七頁，共一百二十四頁，2022年，8月28日置換-（4）例子：E=P(x,y,z),={a/x,f(b)/y,c/z}E=P(a,f(b),c)E=P(x,g(y),h(x,z)),={a/x,f(b)/y,g(w)/z}E=P(a,g(f(b)),h(a,g(w)))E=P(x,y,z),={y/x,z/y}E=P(y,z,z).EP(z,z,z).(同時)第三十八頁，共一百二十四頁，2022年，8月28日置換的復(fù)合（乘積）（1）例子:E=P(x,y,z)={a/x,f(z)/y,w/z}E=P(a,f(z),w)={t/z,g(b)/w}E=P(a,f(t),g(b))={a/x,f(t)/y,g(b)/z}第三十九頁，共一百二十四頁，2022年，8月28日置換的復(fù)合（乘積）（2）定義：設(shè)={t1/x1,t2/x2,…,tn/xn}和={u1/y1,u2/y2,…,um/ym}是兩個置換,

也是一個置換,可定義為:先作置換:{t1

/x1,t2

/x2,…,tn

/xn,u1/y1,u2/y2,…,um/ym}若:yi

(x1,x2,…,xn)則刪除ui/yi若:ti

=xi,則刪除ti

=xi所得的置換稱為和的復(fù)合或乘積,記為?第四十頁，共一百二十四頁，2022年，8月28日置換的復(fù)合（乘積）-（3）定理：設(shè)和是兩個置換,E是表達式，則E(

)=(E)

設(shè),,是三個置換,則有:置換滿足結(jié)合率:(?)?=?(?)

置換的交換率不成立?=?=第四十一頁，共一百二十四頁，2022年，8月28日置換的復(fù)合（乘積）-（4）={a/x},={b/x}={a/x}={b/x}第四十二頁，共一百二十四頁，2022年，8月28日合一（Unification）（1）定義:設(shè)有公式集E={E1,...,En}和置換,使得:E1=E2=…=En則稱E1,...,En是可合一的,并且稱為一合一置換.也稱為{E1,…,En}的合一子(unifier).定義：如果對{E1,…,En}存在這樣的合一子,則稱集合{E1,…,En}是可合一的.第四十三頁，共一百二十四頁，2022年，8月28日合一（Unification）（2）例1:E={P(a,y),P(x,f(b))},={a/x,f(b)/y}.E={P(a,b),P(x,f(b))}合一子不一定唯一E={P(a,y),P(x,f(b))}1={a/x,f(b)/y}(唯一)E={P(x,y),P(x,f(b))}1={a/x,f(b)/y}(不唯一)2={b/x,f(b)/y}第四十四頁，共一百二十四頁，2022年，8月28日最一般合一（1）定義:設(shè)是公式集E的一個合一,如果對于任一個合一,都存在置換使得:=?,則稱是公式集E的最一般合一置換,記為mgu(mostgeneralunifier)第四十五頁，共一百二十四頁，2022年，8月28日最一般合一（2）例子:E={P(x,y),P(x,f(b))}1={a/x,f(b)/y}2={b/x,f(b)/y}={f(b)/y}1={a/x}2={b/x}第四十六頁，共一百二十四頁，2022年，8月28日差異集合設(shè)W是非空表達式集合，W的差異集合D定義如下：首先找出W的所有表達式中不是都相同的第一個符號，然后從W的每個表達式中抽出占有這個符號位置的子表達式，所有這些子表達式組成的集合就是W的差異集合D。若D中無變量符號，則W是不可合一的若D中只有一個元素，則W是不可合一的若D中的變量符號x和t，且x出現(xiàn)在t中，則W是不可合一的例子:W={P(x,f(y,z),z，w),P(x,a),P(x,g(z),z,b)}D={f(y,z),a,g(z)}第四十七頁，共一百二十四頁，2022年，8月28日合一算法（1）(1)令k=0,W0=W(W={E1,E2}),

0=(2)如果Wk已經(jīng)合一,則算法停止,

k=mgu否則，求出Wk的差異集Dk(3)如果Dk中存在元素xk,

tk,且xk不在tk中出現(xiàn),則轉(zhuǎn)(4)；否則不可合一，停止(4)令

k+1=

k?{tk/xk}Wk+1=Wk{tk/xk}=W

k+1(5)k=k+1然后轉(zhuǎn)(2)第四十八頁，共一百二十四頁，2022年，8月28日合一算法（2）換名:{P(f(x),x),P(x,a)};如果不換名：D={f(x),x}.換名:{P(f(y),y),P(x,a)};mgu:{f(a)/x,a/y}第四十九頁，共一百二十四頁，2022年，8月28日合一算法（3）求W={P(a,x,f(g(y))),P(z,f(z),f(u))}的mgu.D0={a,z}.

1=

{a/z}={a/z}.W1=W0

1={P(a,x,f(g(y))),P(a,f(a),f(u))}D1={x,f(a)}.

2=

1{f(a)/x}={a/z,f(a)/x}.W2=W1

2={P(a,f(a),f(g(y))),P(a,f(a),f(u))}D2={g(y),u}.

3=

2{g(y)/u}={a/z,f(a)/x,g(y)/u}W3=W2

3={P(a,f(a),f(g(y)))}

3是mgu.第五十頁，共一百二十四頁，2022年，8月28日合一算法（4）求W={Q(f(a),g(x)),Q(y,y)}的mgu.D0={f(a),y}.

1=

{f(a)/y}={f(a)/y}.W1=W0

1={Q(f(a),g(x)),Q(f(a),f(a))}D1={g(x),f(a)}.不可合一,沒有mgu.第五十一頁，共一百二十四頁，2022年，8月28日合一算法（5）求W={P(f(y),y),P(x,a)}的mgu.D0={f(y),x}.

1=

{f(y)/x}={f(y)/x}.W1=W0

1={P(f(y),y),P(f(y),a)}D1={y,a}.

2=

1{a/y}={f(y)/x}{a/y}={f(a)/x,a/y}.W2=W1

2={P(f(a),a)}

2是mgu.第五十二頁，共一百二十四頁，2022年，8月28日合一算法（6）性質(zhì)：若W是關(guān)于表達式的有限非空可合一集合，則合一算法將在第（2）步結(jié)束，并且最后的

k是W的mgu。若一組表達式E1,…,En是可合一的，則它們的mgu除了相差一個改名外，是唯一確定。第五十三頁，共一百二十四頁，2022年，8月28日歸結(jié)式定義:設(shè)C1和C2是兩個無公共變量的子句,L1和L2分別是C1和C2的文字,如果L1和~L2有mgu:,則:(C1-{L1})(C2-{L2})稱為C1和C2的一個二元歸結(jié)式,而L1L2稱為被歸結(jié)的文字若R(C1,C2)是C1,C2的二元歸結(jié)式,則:C1C2=>R(C1,C2)第五十四頁，共一百二十四頁，2022年，8月28日歸結(jié)式--例子（1）C1:P(x)Q(x)C2:~P(a)R(x)重命名C2:~P(a)R(y)L1=P(x),L2=~P(a)L1與~L2有mgu={a/x}(C1–L1)(C2–L2)=({P(a),Q(a)}–{P(a)})({~P(a),R(y)}–{~P(a)})={Q(a)}{R(y)}={Q(a),R(y)}Q(a)

R(y)是C1與C2的二元歸結(jié)式.第五十五頁，共一百二十四頁，2022年，8月28日歸結(jié)式--例子（2）C1=P(x)Q(x)

C2=~P(g(y))~Q(b)R(x)1={g(y)/x}:R(C1,C2)=Q(g(y))~Q(b)R(x)2={b/x}:R(C1,C2)=~P(g(y))P(b)R(x)第五十六頁，共一百二十四頁，2022年，8月28日歸結(jié)式—因子定義：如果一個子句C的幾個文字有mgu,則C稱為子句C的因子例子

設(shè)C=P(x)P(f(y)~Q(x)假設(shè)={f(y)/x},則:C=P(f(y))~Q(f(y))第五十七頁，共一百二十四頁，2022年，8月28日歸結(jié)式定義:設(shè)C1和C2是無公共變量的子句,其歸結(jié)式是下列二元歸結(jié)式之一:(1)C1和C2的二元歸結(jié)式(2)C1的因子和C2的二元歸結(jié)式(3)C1和C2的因子的二元歸結(jié)式(4)C1的因子和C2的因子的二元歸結(jié)式該歸結(jié)式仍記為R(C1,C2)第五十八頁，共一百二十四頁，2022年，8月28日歸結(jié)式-2例:C1=P(x)P(f(y)Q(g(y))C2=~P(f(g(x)))Q(b)

C1的因子為:

={f(y)/x},C1=P(f(y))Q(g(y))則:R(C1,C2)=Q(g(g(x)))Q(b)第五十九頁，共一百二十四頁，2022年，8月28日歸結(jié)反演設(shè)E為已知前提的公式集,Q為目標(biāo)公式(或結(jié)論),用歸結(jié)反演證明Q為真的步驟為:(1)否定Q得到~Q(2)把~Q加入到公式集E中,得到{E,~Q}(3)把公式集{E,~Q}化為子句集S(4)應(yīng)用歸結(jié)原理對子句集S中的子句進行歸結(jié),并把每次歸結(jié)所得的歸結(jié)式并入S中.如此反復(fù)進行,若出現(xiàn)空子句,則停止歸結(jié),此時就證明了Q為真.第六十頁，共一百二十四頁，2022年，8月28日歸結(jié)反演—示例一已知：求證：第六十一頁，共一百二十四頁，2022年，8月28日歸結(jié)反演—示例二給定下面一段話：

Tony、Mike和John都是AlpineClub的會員。每個會員或者是一個滑雪愛好者，或者是一個登山愛好者，或者都是。沒有一個登山愛好者喜歡下雨，所有的滑雪愛好者都喜歡雪。Tony喜歡的所有東西Mike都不喜歡，Tony不喜歡的所有東西Mike都喜歡。Tony喜歡雨和雪。用謂詞演算表達上述信息。把問題“誰是該俱樂部的會員，他是一個登山愛好者，但不是滑雪愛好者”表達為一個謂詞表達式，用歸結(jié)反駁提取答案第六十二頁，共一百二十四頁，2022年，8月28日歸結(jié)的完備性問題的提出：若定理成立，是否使用歸結(jié)方法必能得到證明？或者說：使用歸結(jié)方法推出的定理的個數(shù)和所有成立的定理的個數(shù)是否一樣多？第六十三頁，共一百二十四頁，2022年，8月28日Herbrand定理由來為了評定子句集的不可滿足性,就需要對子句集中的子句進行評定.一般情況下,要評定一個子句的不可滿足性,需要對個體域上的一切解釋逐個地進行評定.但是由于個體變量論域的任意性,以及解釋個數(shù)的無限性,因此評定子句集的不可滿足性是很困難的.Herbrand域就是一個特殊的域,只要在這個論域上公式不可滿足,則該公式就在任一論域上也不可滿足第六十四頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域定義:設(shè)S為子句集,則按下述方法構(gòu)造的域H稱為H域:(1)令H0是S中所有的個體常量的集合,若S中不包含個體常量,則任取常量aD,而規(guī)定H0={a}(2)令Hi+1=Hi{所有形如f(t1,…,tn)的元素}其中:f(t1,…,tn)是出現(xiàn)于S中的任一函數(shù),而t1,…,tn是Hi中的元素.i=1,2,….H域是直接依賴于S的最多只有可數(shù)個元素第六十五頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域例一:S={P(a),~P(x)P(f(x))}根據(jù)定義有: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)),…}.例二:S={~P(x),~Q(y)R(z)}H0=H1=…=H={a}第六十六頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域例三：S={P(f(x)，a，g(y)，b)}H0={a，b}

H1={a，b，f(a)，g(a)，f(b)，g(b)}

H2={a，b，f(a)，g(a)，f(b)，g(b)，f(f(a))，f(g(a))，f(f(b))，f(g(b))，g(f(a))，g(g(a))，g(f(b))，g(g(b))}

...

第六十七頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域基礎(chǔ)(ground)/基沒有變量的項稱為基礎(chǔ)項(groundterm).f(a,b)沒有變量的原子稱為基礎(chǔ)原子(groundatom).P(a,f(b))沒有變量的文字稱為基礎(chǔ)文字(groundliteral).P(a,f(b)),~P(a,f(b))沒有變量的子句稱為基礎(chǔ)子句(groundclause).P(b,f(b))~Q(f(f(b)))第六十八頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域原子集:子句中所有基原子構(gòu)成的集合稱為原子集.令S是一個子句集合,形如P(t1,...,tn)的基礎(chǔ)原子集合,稱為S的原子集.記為A.

其中,P(t1,...,tn)是出現(xiàn)在S中的任一謂詞符號,而t1,...,tn是S的H域的任意元素。第六十九頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域S={P(z),P(x)∨Q(y)}H∞={a}A={P(a),Q(a)}S={P(a),P(x)∨P(f(x))}H∞={a,f(a),f(f(a)),...}A={P(a),P(f(a)),P(f(f(a))),...}S={P(f(x),a,g(y),b)}H∞={a,b,f(a),g(a),f(b),g(b),…}A={P(a,a,a,a),P(a,a,a,b),P(a,a,b,b),...}第七十頁，共一百二十四頁，2022年，8月28日Herbrand定理--H域定義(基礎(chǔ)實例)當(dāng)S中的某子句C中所有變量符號均以S的H域的元素代入時，所得的基子句C’稱作C的一個基礎(chǔ)實例(基例）例S={P(x),Q(f(y))∨R(y),Z(f(y))}H={a,f(a),f(f(a)),...}P(a),P(f(a))都稱作子句C=P(x)的基例。同樣,Q(f(a))∨R(a),Q(f(f(a)))∨R(f(a))都是Q(f(y))∨R(y)的基例。Q(a)∨R(a)不是Q(f(y))∨R(y)的基例。對于任一b∈D,子句P(b),Q(f(b))∨R(b)都叫基子句。第七十一頁，共一百二十四頁，2022年，8月28日Herbrand定理--H的解釋起因由子句集S建立H域、原子集A;一般論域D上對S的解釋IH域上的解釋I*;S在D上為真S在H上為真;S在D上不可滿足S在H上不可滿足;第七十二頁，共一百二十四頁，2022年，8月28日Herbrand定理--H的解釋H解釋的表示令A(yù)={A1,…,An,…}是S的原子集,一個H解釋可被表示為:

I={m1,…,mn,…}

其中mj或者是Aj或者是~Aj.

如果mj是Aj,則Aj為真,否則,Aj為假.第七十三頁，共一百二十四頁，2022年，8月28日Herbrand定理--H的解釋定義:子句集S在H域上的一個解釋I*滿足下列條件:(1)在解釋I*下,常量映射到自身(2)S中的任一n元函數(shù)是HnH的映射.即假設(shè)h1,h2,…,hnH,則f(h1,h2,…,hn)H(3)S中的任一個n元謂詞是Hn{T,F}的映射.第七十四頁，共一百二十四頁，2022年，8月28日Herbrand定理--H的解釋例子:S={P(x)Q(x),R(f(y))}H={a,f(a),f(f(a)),…}.A={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),…}S的H解釋,如:I*1={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),…}I*2={~P(a),~Q(a),~R(a),~P(f(a)),~Q(f(a)),R(f(a)),…}I*3={P(a),~Q(a),~R(a),P(f(a)),Q(f(a)),~R(f(a)),…}則有:S|I*1=T,S|I*2=F,S|I*3=F第七十五頁，共一百二十四頁，2022年，8月28日Herbrand定理--H的解釋由S在D域的解釋I如何確定相應(yīng)的S在H域的解釋I*:(1)若S中有常量符號,任一aH0,在I下a取值為a0,就規(guī)定aa0(2)若S中無常量符號,H0={a},就規(guī)定aa0,a0是D的任一元素(3)若f(h1,h2,…,hn)是S中的任一函數(shù)符號,任取(h1,h2,…,hn)Hni.當(dāng)在I下(h1,h2,…,hn)取值為(h01,h02,…,h0n),且在I下對應(yīng)值為f(h01,h02,…,h0n)(為D中的元素),就規(guī)定:f(h1,h2,…,hn)f(h01,h02,…,h0n)則I*是如下的H解釋：

VI*(P(h1,h2,…,hn))=VI(P(h01,h02,…,h0n))第七十六頁，共一百二十四頁，2022年，8月28日Herbrand定理--H的解釋定理:設(shè)I是S的論域D上的解釋,存在對應(yīng)于I的H解釋I*,使得如果S|I=T,則有S|I*=T定理:子句集S是不可滿足的,當(dāng)且僅當(dāng)在所有的S的H解釋下為假()設(shè)S是不可滿足的.則在任一個論域上的任一解釋使S為假;H是一個論域;()設(shè)S的所有的H解釋使S為假.假設(shè)子句集S可滿足.在某個論域上的某個解釋I使S為真;I在H域上對應(yīng)解釋I*;根據(jù)引理，I*滿足S.第七十七頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹語義樹是通過將S的所有解釋展示在一棵樹上,從幾何上對S的不可滿足性進行討論Example1G=PQRS={P,

Q,R}A={P,

Q,R}P~PQ~QQ~QR~RR~RR~RR~R第七十八頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹Example2S={~P(x)Q(x),P(f(y)),~Q(f(y))}H={a,f(a),f(f(a)),...}A={P(a),Q(a),P(f(a)),Q(f(a)),...}P(a)~P(a)Q(a)~Q(a)Q(a)~Q(a)P(f(a))~P(f(a))P(f(a))~P(f(a))P(f(a))~P(f(a))…….……

……

……第七十九頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹顛倒原子的順序是可以的.例如Q(a)為第一個頂點.如果原子集是無限的，則對應(yīng)的語義樹必定是無限的.從任一個葉節(jié)點向根節(jié)點看,代表S的一個解釋.從任一個中間節(jié)點向根節(jié)點看,代表S的一個部分解釋.第八十頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹語義樹的特點:S的語義樹是完全的,如果N表示葉節(jié)點,則I(N)包含了S的原子集中所有元素或者該元素的否定語義樹每個直到葉節(jié)點的分枝都對應(yīng)于S的一個解釋.特別對有限樹來說,I(N)就是S的一個解釋如果節(jié)點N的I(N)使S的某一子句的某一集子句為假,而N的父輩節(jié)點不能評定這個事實,則稱N為失敗節(jié)點如果S的完全語義樹的每個分枝上都有一個失敗節(jié)點,就說該語義樹為封閉語義樹第八十一頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹ExampleS={P,QR,~P~Q,~P~R}P~PQ~QQ~QR~RR~RR~RR~R第八十二頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹封閉語義樹：P~PQ~QR~R第八十三頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹ExampleS={P(x),~P(x)Q(f(x)),~Q(f(a))}A={P(a),Q(a),P(f(a)),Q(f(a)),…}P(a)Q(f(a))~P(a)~Q(f(a))第八十四頁，共一百二十四頁，2022年，8月28日Herbrand定理--語義樹證明一個定理就是尋找一棵封閉語義樹.S不可滿足S在所有解釋下為假S在所有H解釋下為假;完備語義樹包含所有H解釋;每一枝是一個H解釋;S在I下為假,則使某個基礎(chǔ)實例為假;這個節(jié)點稱為假節(jié)點,不用再擴展;所有枝上都有假節(jié)點,則為封閉語義樹;第八十五頁，共一百二十四頁，2022年，8月28日Herbrand定理Herbrand定理(1):子句集S是不可滿足的,當(dāng)且僅當(dāng)對應(yīng)于S的完全語義樹都是一棵有限封閉語義樹第八十六頁，共一百二十四頁，2022年，8月28日Herbrand定理Herbrand定理(2):子句集S是不可滿足的,當(dāng)且僅當(dāng)存在不可滿足的S的有限基例集S‘例子:S={P(x),~P(a)~P(b),Q(f(x))}H={a,b,f(a),f(b),f(f(a)),f(f(b))…}A={P(a),P(b),Q(a),Q(b),…}S’={P(a),P(b),~P(a)~P(b)}P(a)P(b)~P(a)~P(b)第八十七頁，共一百二十四頁，2022年，8月28日困難生成基礎(chǔ)實例集合是指數(shù)復(fù)雜性的例子:

S={P(x,g(x),y,h(x,y),z,k(x,y,z)),~P(u,v,e(v),w,f(v,w),x)}H0={a}H1={a,g(a),h(a,a),k(a,a,a),e(a),f(a,a)}基礎(chǔ)實例集：S0={P(a,g(a),a,h(a,a),a,k(a,a,a)),~P(a,a,e(a),a,f(a,a),a)}S1有6*6*6+6*6*6*6=1512個元素;H5有1064數(shù)量級的元素，S5有10256數(shù)量級的元素.第八十八頁，共一百二十四頁，2022年，8月28日

一些簡化計算規(guī)則(1)重言式子句可刪除規(guī)則S中的重言式子句，不會為S的不可滿足提供任何信息，可以刪除S={P∨~P，Q，R∨P}

S的邏輯含義是（P∨~P）∧Q∧(R∨P)=Q∧(R∨P)，從而刪去重言式P∨~P，不影響S的真值。S’={Q，R∨P}第八十九頁，共一百二十四頁，2022年，8月28日

一些簡化計算規(guī)則(2)單文字刪除規(guī)則單文字:在S中存在只有一個文字的基礎(chǔ)子句L.如S={L,LC1,~LC2,C3,C4},其中C3,C4不含L和~L.從S中刪除含L的子句得到:S‘={~LC2,C3,C4}從S’中刪除文字~L得到:S={C2,C3,C4}若S’為空,則S是可滿足的若S‘不空,則S和S同時是不可滿足的.第九十頁，共一百二十四頁，2022年，8月28日

一些簡化計算規(guī)則(3)純文字刪除規(guī)則定義:當(dāng)文字L出現(xiàn)于S中,而~L不出現(xiàn)于S中時,則稱L為S的純文字從S中刪除含L的子句得S‘.

如果S‘為空集,則S是可滿足的如果S‘非空,則S與S’同時是不可滿足的例子:S={A∨B,A∨~B,~B,B}S’={~B,B};第九十一頁，共一百二十四頁，2022年，8月28日

一些簡化計算規(guī)則(4)分離規(guī)則若S=(LA1)

…(LAm)

(~LB1)

…(~LBn)

R其中R是不含L和~L的文字集令S‘={A1,.…,Am,R}S=(B1,…,Bn,R}則S不可滿足當(dāng)且僅當(dāng)S‘和同時不可滿足S第九十二頁，共一百二十四頁，2022年，8月28日

一些簡化計算規(guī)則(5)S={PQ~R,P~Q,~P,R,U}對U使用純文字:{PQ~R,P~Q,~P,R}對~P使用單文字:{Q~R,~Q,R}對~Q使用單文字:{~R,R}對R使用單文字:{}S不可滿足;S={PQ,~Q,~PQ~R}對~Q使用單文字:{P,~P~R}對P使用單文字:{~R}對~R使用純文字:{}S可滿足；第九十三頁，共一百二十四頁，2022年，8月28日歸結(jié)和語義樹“倒塌”過程例：S={P,~P∨Q,~P∨~Q}A={P,Q}歸結(jié)過程：(1)P(2)~P∨Q(3)~P∨~Q(4)~P(2)(3)(5)□(1)(4)PQN11N12N21N24TN0PQN11N12N21T*N0PN11T(1)第九十四頁，共一百二十四頁，2022年，8月28日歸結(jié)的完備性提升引理:C1、C2是無公共變量的子句，而C1’、C2’分別是C1、C2的例，R’是C1’、C2’的歸結(jié)式，則存在C1、C2的歸結(jié)式R，使得R’是R的例第九十五頁，共一百二十四頁，2022年，8月28日歸結(jié)的完備性例子C1:P(x)Q(f(x))C2:~Q(y)R(y)

C1’:P(a)Q(f(a)){a/x}C2’:~Q(f(a))R(f(a))

{f(a)/y}C’:P(a)R(f(a))C:P(x)R(f(x))第九十六頁，共一百二十四頁，2022年，8月28日歸結(jié)的完備性完備性定理：S是不可滿足的當(dāng)且僅當(dāng)存在一個使用歸結(jié)推理規(guī)則的從S到空子句?的推理過程第九十七頁，共一百二十四頁，2022年，8月28日效率的問題（1）歸結(jié)原理比Herbrand定理有了明顯的進步;盲目的歸結(jié)會產(chǎn)生組合爆炸問題;不必要的歸結(jié)式不必要的歸結(jié)式;第九十八頁，共一百二十四頁，2022年，8月28日效率的問題（2）S={PQ,~PQ,P~Q,~P~Q}盲目歸結(jié)過程:S0=SSi={C1,C2的歸結(jié)式|C1S0S1…Si-1,C2Si-1}具體過程:S0:(1)PQ(2)~PQ(3)P~Q(4)~P~QS1:(5)Q(1)(2)(6)P(1)(3)(7)Q~Q(1)(4)(8)P~P(1)(4)…….(12)~QS2:(13)PQ(1)(7)(14)PQ(1)(8)…….(39)nil(5)(12)第九十九頁，共一百二十四頁，2022年，8月28日Agenda引言命題邏輯中的歸結(jié)原理謂詞邏輯中的歸結(jié)原理非單調(diào)推理第一百頁，共一百二十四頁，2022年，8月28日非單調(diào)推理什么是非單調(diào)推理

主要的非單調(diào)邏輯封閉世界假設(shè)(CWA)限制理論缺省邏輯第一百零一頁，共一百二十四頁，2022年，8月28日什么是非單調(diào)推理(1)科學(xué)的發(fā)現(xiàn)過程是一個證偽的過程，人類知識的增長是一個非單調(diào)的過程傳統(tǒng)的邏輯系統(tǒng)實際上作的是單調(diào)推理，加進系統(tǒng)的新知識（信念）必須與已有的知識（信念）相一致，不會引起矛盾。所以，隨著運行時間的推移，系統(tǒng)內(nèi)含的知識有增無減，這就是所謂的單調(diào)性。

設(shè)FS為一個邏輯系統(tǒng)，如果對于FS的任意兩個公式集合T和S，T是S的子集，則Th(T)也是Th(S)的子集(Th(T)表示從T中推出的定理的集合={A|TA})這說明向一個公理理論中增加新的定理不會影響該理論已經(jīng)有的定理，初始理論原來已經(jīng)有的定理仍然是擴大了以后理論的定理。

第一百零二頁，共一百二十四頁，2022年，8月28日什么是非單調(diào)推理(2)單調(diào)性的優(yōu)點在于：（1）加入新命題時不需審查與系統(tǒng)原有知識的相容性，因為這些新命題只能是已有知識的邏輯推理結(jié)果，不可能引起矛盾。換言之，加入的新命題必定是永真的。（2）不需要記憶推導(dǎo)過程。因為推導(dǎo)的結(jié)論永遠不會失敗，不存在事后審查推導(dǎo)過程的需求問題。第一百零三頁，共一百二十四頁，2022年，8月28日什么是非單調(diào)推理(3)非單調(diào)性推理推理系統(tǒng)的定理集合并不隨推理過程的進行而增大，新推出的定理很可能會否定、改變原來的一些定理。推理時所依據(jù)的知識具有不完全性

邏輯系統(tǒng)是非單調(diào)的，如果存在公式集合T和S，如果TS，但Th(T)Th(S)第一百零四頁，共一百二十四頁，2022年，8月28日什么是非單調(diào)推理(4)需要非單調(diào)推理的理由主要為：知識的不完全

一個有限的信念集合僅僅是現(xiàn)實世界的近似描述，會有很多的例外----資格問題

客觀世界變化太快，一個不斷變化的世界必須用變化的知識庫加以描述

–框架問題非單調(diào)推理比單調(diào)推理難處理得多。因為當(dāng)一個假設(shè)被發(fā)現(xiàn)錯誤而撤消時，一系列基于它的推理結(jié)果都要撤消。所以，設(shè)計非單調(diào)推理系統(tǒng)的一個關(guān)鍵問題在于防止系統(tǒng)花費過多的時間在這種處理上。

第一百零五頁，共一百二十四頁，2022年，8月28日什么是非單調(diào)推理(5)非單調(diào)推理的研究有兩條途徑：對邏輯的擴展：這涉及非單調(diào)推理的形式化方面，稱為非單調(diào)邏輯，它包括：語言方面的擴充（指增強其表達能力）和語義方面的擴充（指對真值的真假兩種情況進行修正）；主要包括：基于最小化語義：主要有封閉世界假設(shè)、McCarthy的限制邏輯（circumscription）、Konolige的忽略邏輯等基于定點定義：主要有缺省邏輯(default)和自認知邏輯(autoepistemic)等。對推理模式的擴展：這涉及非單調(diào)推理的過程化方面，稱為非單調(diào)系統(tǒng)。這可以通過對矛盾的檢測進行真值的修正來維護相容性，可稱為真值維護系統(tǒng)。第一百零六頁，共一百二十四頁，2022年，8月28日什么是非單調(diào)推理(6)非單調(diào)推理的三個主要流派：McCarthy的限制理論：當(dāng)且僅當(dāng)沒有事實證明S在更大的范圍成立時，S只在指定的范圍成立；Reiter的缺省邏輯：“S在缺省的條件下成立”是指“當(dāng)且僅當(dāng)沒有事實證明S不成立時S是成立的”。Moore的自認知邏輯：“如果我知道S，并且我不知道有其他任何事實與S矛盾，則S是成立的”。第一百零七頁，共一百二十四頁，2022年，8月28日封閉世界假設(shè)(1)在非單調(diào)領(lǐng)域中的推理，我們必須給出下面的假設(shè)：封閉世界假設(shè)（ClosedWorldAssumption:CWA），或者增加新的事實，繼續(xù)推理封閉世界假設(shè)是一種對由一組基本信念集合KB定義的理論T(KB)進行完備化的方法。我們說一個理論T(KB)是完備的，是說其包含（顯式或隱含）了每一個基原子公式或該公式否定。CWA的基本思想是：如果無法證明P，則就認為它是否定的。即：如果從知識庫中無法證明P或者P，則就向KB中增加P即假定知道所有有關(guān)世界的事情（世界是封閉的）第一百零八頁，共一百二十四頁，2022年，8月28日封閉世界假設(shè)(2)CWA是非單調(diào)的：CWA對理論的完備化是僅僅通過向基本信念集合KB中增加基原子公式的取反來實現(xiàn)的。一旦以后有新的基原子公式加進KB，則為完備T（KB）而生成的擴充集就必須收縮（刪除該基原子公式的否定）。

由于為完備T(KB)而生成的擴充集中的每個基原子公式的取反均是假設(shè)的暫時信念，記該擴充集為KBasm。對于一個基原子公式P，CWA可定義：PKBasm，當(dāng)且僅當(dāng)PT(KB)。經(jīng)過由CWA方法完備的理論為CWA(KB),它擴大了T(KB)的推理能力,允許不能由KB導(dǎo)出的結(jié)論可以由KBKBasm導(dǎo)出.第一百零九頁，共一百二十四頁，2022年，8月28日封閉世界假設(shè)(3)CWA方法并不確保被完備的理論CWA(KB)是一致的，解決不一致性是非單調(diào)推理的重要議題，需要對CWA的完備性規(guī)則進行修改，以實現(xiàn)一致性。CWA(KB)是一致的，當(dāng)且僅當(dāng)對于每個可由KB推導(dǎo)出的子句P1P2…Pn，都至少存在一個Pi可從KB推導(dǎo)出；其中Pi均為正基文字。若KB是由一致的Horn形子句組成時，則CWA(KB)必定一致第一百一十頁，共一百二十四頁，2022年，8月28日限制理論（1）限制理論的核心思想是：如果一個句子敘述一個命題，那么它敘述的僅僅是這個命題，一點都不能擴張和延伸，任何多余的東西都要刪除掉。這就是所謂的“Occam剃刀原理”，McCarthy稱為極小模型。限制理論最初是用于定義通常什么事物是成立的這可以在FOL中定義一個”盡可能錯”的特殊異常的謂詞：ab然后通過最小化ab的擴展，最小化該異常性即除了那些已知為真的對象外，其他都為假第一百一十一頁，共一百二十四頁，2022年，8月28日限制理論（2）and_gate(x,in1,in2,out)zero(in1)?ab(x)

zero(out)block(x)?ab(x)ontable(x)holds(F,t)?ab(F,t+1)holds(F,t+1)第一百一十二頁，共一百二十四頁，2022年，8月28日限制理論（3）限制有多種形式，如：平行限制（公式限制）論域限制謂詞限制……第一百一十三頁，共一百二十四頁，2022年，8月28日平行限制限制作為二階公式：令P=Q表示x(P(x)Q(x))令PQ表示x(P(x)Q(x))令P<Q表示(PQ)?(P=Q)令A(yù)(P)表示包含謂詞P的句子A中P的限制CIRC(A;P)為：A(P)?q[A(q)q<P]直覺