第5章-基于謂詞邏輯的機(jī)器推理課件-002_第1頁
第5章-基于謂詞邏輯的機(jī)器推理課件-002_第2頁
第5章-基于謂詞邏輯的機(jī)器推理課件-002_第3頁
第5章-基于謂詞邏輯的機(jī)器推理課件-002_第4頁
第5章-基于謂詞邏輯的機(jī)器推理課件-002_第5頁
已閱讀5頁,還剩145頁未讀, 繼續(xù)免費(fèi)閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報或認(rèn)領(lǐng)

文檔簡介

第5章基于謂詞邏輯的機(jī)器推理7/24/20231目錄5.0機(jī)器推理概述5.1一階謂詞邏輯5.2歸結(jié)演繹推理5.3應(yīng)用歸結(jié)原理求取問題答案5.4歸結(jié)策略5.5歸結(jié)反演程序舉例*5.6Horn子句歸結(jié)與邏輯程序5.7非歸結(jié)演繹推理7/24/202325.0機(jī)器推理概述(1)機(jī)器推理:就是計算機(jī)推理,也稱自動推理。它是人工智能的核心課題之一。推理是人腦的一個基本功能和重要功能。幾乎所有的人工智能領(lǐng)域都與推理有關(guān)。因此,要實(shí)現(xiàn)人工智能,就必須將推理的功能賦予機(jī)器,實(shí)現(xiàn)機(jī)器推理。自動定理證明:是機(jī)器推理的一種重要應(yīng)用,它是利用計算機(jī)證明非數(shù)值性的結(jié)果,很多非數(shù)值領(lǐng)域的任務(wù)如醫(yī)療診斷、信息檢索、規(guī)劃制定和難題求解等方法都可以轉(zhuǎn)化一個定理證明問題。7/24/20233自動定理證明的基本方法:5.0機(jī)器推理概述(2)定理證明器:它是研究一切可判定問題的證明方法。魯濱遜的歸結(jié)原理。人機(jī)交互進(jìn)行定理證明:計算機(jī)作為數(shù)學(xué)家的輔助工具,用計算機(jī)幫助人完成手工證明中的難以完成的煩雜的大量計算推理和窮舉。四色定理。判定法:該方法是對一類問題找出統(tǒng)一的計算機(jī)上可實(shí)現(xiàn)的算法。數(shù)學(xué)家吳文俊教授——吳氏方法。自然演繹法:該方法依據(jù)推理規(guī)則從前提和公理中可以推出許多定理,如果待證明的定理在其中則定理得證。LT程序、證明平面幾何的程序。7/24/20234基于歸結(jié)原理的自動定理證明過程:5.0機(jī)器推理概述(3)定理的自然語言描述定理的謂詞公式描述子句集生成子句集定理得證應(yīng)用歸結(jié)規(guī)則+歸結(jié)策略自然語言處理生成謂詞公式已知前提:(1)自然數(shù)都是大于零的整數(shù)。(2)所有整數(shù)不是偶數(shù)就是奇數(shù)。(3)偶數(shù)除以2是整數(shù)。結(jié)論:所有自然數(shù)不是奇數(shù)就是一半為整數(shù)的數(shù)。7/24/202355.0機(jī)器推理概述(4)本章主要解決以下幾個問題:1、一階謂詞邏輯及基于一階謂詞邏輯的知識表示2、謂詞公式到子句集的轉(zhuǎn)換3、命題邏輯和謂詞邏輯中的歸結(jié)原理4、歸結(jié)策略7/24/202365.1一階謂詞邏輯5.1.1謂詞、函數(shù)、量詞5.1.2謂詞公式5.1.3謂詞邏輯中的形式演繹推理7/24/202375.1.1謂詞、函數(shù)、量詞(1)命題(proposition):是具有真假意義的語句。命題代表人們進(jìn)行思維時的一種判斷,或者是否定,或者是肯定。命題可以用命題符號表示。用命題符號可以表示簡單的邏輯關(guān)系和推理。

P:今天天氣好Q:去旅游S1:我有名字S2:你有名字PQ表示:如果今天天氣好,就去旅游。此時,如果P(今天天氣好)成立,則可以得到結(jié)論Q(去旅游)7/24/202385.1.1謂詞、函數(shù)、量詞(2)對于復(fù)雜的知識,命題符號能力不夠。無法把所描述的客觀事物的結(jié)構(gòu)及邏輯特征反映出來。無法把不同事物間的共同特征表達(dá)出來。F:老李是小李的父親。S1:我有名字S2:你有名字所有的人都有名字:SIS2S3…

7/24/202395.1.1謂詞、函數(shù)、量詞(3)謂詞(predicate):一般形式為P(x1,x2,…,

xn)P為謂詞名,用于刻畫個體的性質(zhì)、狀態(tài)或個體間的關(guān)系。x1,x2,…,

xn是個體,表示某個獨(dú)立存在的事物或者某個抽象的概念。S(x):x是學(xué)生;P(x,y):x是y的雙親。個體變元的變化范圍稱為個體域。包攬一切事物的集合稱為全總個體域。7/24/2023105.1.1謂詞、函數(shù)、量詞(4)函數(shù):為了表達(dá)個體之間的對應(yīng)關(guān)系,引入數(shù)學(xué)中函數(shù)概念和記法。用形如f(x1,x2,…,xn)來表示個體變元對應(yīng)的個體y,并稱之為n元個體函數(shù),簡稱函數(shù)。函數(shù)father(x):值為x的父親。謂詞D(father(x)):表示x的父親是醫(yī)生,值為真或假。符號約定:謂詞-大寫字母;P(x,y)函數(shù)-小寫字母;f(x)變量-x、y、z、u、v……;常量-a、b、c…….。P(a,Y)7/24/2023115.1.1謂詞、函數(shù)、量詞(5)表示“對個體域中所有的(或任一個)個體”。記為x全稱量詞表示“在個體域中存在個體”。記為x存在量詞如:“凡是人都有名字”

用M(x)表示“x是人”,N(x)表示“x有名字”x(M(x)N(x))如:“存在不是偶數(shù)的整數(shù)”用G(x)表示“x是整數(shù)”,E(x)表示“x是偶數(shù)”x(G(x)?E(x))7/24/2023125.1.1謂詞、函數(shù)、量詞(6)用謂詞表示命題時,一般取全總個體域,再采用使用限定謂詞的方法來指出每個個體變元的個體域。(2)對存在量詞,把限定詞作為一個合取項加入。即x(P(x)…)例:對于所有的自然數(shù),均有x+y>x

xy(N(x)N(y)S(x,y,x))例5.3:某些人對某些食物過敏xy(M(x)N(y)G(x,y))(1)對全稱量詞,把限定詞作為蘊(yùn)含式之前件加入。即x(P(x)…)例5.2:對于所有的自然數(shù),均有x+y>x

也可以用函數(shù)h(x,y)來表示x與y的和

xy(N(x)N(y)G(h(x,y),x))7/24/2023135.1.1謂詞、函數(shù)、量詞(7)例5.1:不存在最大的整數(shù),我們可以把它表示為:

?x(G(x)y(G(y)D(x,y))

x(G(x)y(G(y)D(y,x))用謂詞表示命題時,形式并不是固定的。7/24/2023145.1.1謂詞、函數(shù)、量詞(8)練習(xí):用謂詞公式表示下述命題。已知前提:(1)自然數(shù)都是大于零的整數(shù)。(2)所有整數(shù)不是偶數(shù)就是奇數(shù)。(3)偶數(shù)除以2是整數(shù)。結(jié)論:所有自然數(shù)不是奇數(shù)就是一半為整數(shù)的數(shù)。首先定義如下謂詞:N(x):x是自然數(shù)。I(x):x是整數(shù)。E(x):x是偶數(shù)。

O(x):x是奇數(shù)。GZ(x):x大于零。s(x):x除以2。7/24/2023155.1.1謂詞、函數(shù)、量詞(9)將上述各語句翻譯成謂詞公式:(1)自然數(shù)都是大于零的整數(shù)。F1:x(N(x)GZ(x)I(x))(2)所有整數(shù)不是偶數(shù)就是奇數(shù)。F2:x(I(x)(E(x)O(x)))(3)偶數(shù)除以2是整數(shù)。F3:x(E(x)I(s(x)))所有自然數(shù)不是奇數(shù)就是一半為整數(shù)的數(shù)。G:x(N(x)(I(s(x))O(x)))

7/24/2023165.1.2謂詞公式(1)定義1:項(1)個體常元和變元都是項。(2)f是n元函數(shù)符號,若t1,t2,…,tn是項,則f(t1,t2,…,tn)是項。(3)只有有限次使用(1),(2)得到的符號串才是項。用謂詞、量詞及真值連結(jié)詞可以表達(dá)相當(dāng)復(fù)雜的命題,我們把命題的這種符號表達(dá)式稱為謂詞公式。7/24/2023175.1.2謂詞公式(2)定義2:原子公式設(shè)P為n元謂詞符號,t1,t2,…,tn為項,P(t1,t2,…,tn)稱為原子謂詞公式,簡稱原子或原子公式。7/24/2023185.1.2謂詞公式(3)定義3:謂詞公式(1)原子公式是謂詞公式。(2)若A、B是謂詞公式,則A,AB,AB,AB,A←→B,xA,xA也是謂詞公式。(3)只有有限步應(yīng)用(1)(2)生成的公式才是謂詞公式。謂詞公式亦稱為謂詞邏輯中的合適(式)公式,記為Wff。由項的定義,當(dāng)t1,t2,…,tn全為個體常元時,所得的原子謂詞公式就是原子命題公式(命題符號)。所以全體命題公式也是謂詞公式。

7/24/2023195.1.2謂詞公式(4)轄域:緊接于量詞之后被量詞作用(即說明)的謂詞公式稱為該量詞的轄域。指導(dǎo)變元:量詞后的變元為指導(dǎo)變元。約束變元:在一個量詞轄域中與該量詞的指導(dǎo)變元相同的變元稱為約束變元。自由變元:在一個量詞轄域中與該量詞的指導(dǎo)變元不同的變元稱為自由變元。

(1)xP(x)(2)y(G(y)D(x,y))(3)xG(x)P(x)指導(dǎo)變元約束變元約束變元約束變元自由變元自由變元7/24/2023205.1.2謂詞公式(5)一個變元在一個公式中既可以約束出現(xiàn),也可以自由出現(xiàn),為了避免混淆,通過改名規(guī)則改名:對需要改名的變元,應(yīng)同時更改該變元在量詞及其轄域中的所有出現(xiàn)。新變元符號必須是量詞轄域內(nèi)原先沒有的,最好是公式中也未出現(xiàn)過的。xG(x)P(x)

xG(x)P(y)7/24/2023215.1.2謂詞公式(6)謂詞公式與命題的區(qū)別與聯(lián)系謂詞公式是命題函數(shù)。一個謂詞公式中所有個體變元被量化,謂詞公式就變成了一個命題。從謂詞公式得到命題的兩種方法:給謂詞中的個體變元代入個體常元;把謂詞中的個體變元全部量化。例:P(x)表示“x是素數(shù)”

xP(x),xP(x),P(a)都是命題7/24/2023225.1.2謂詞公式(7)一階謂詞:僅個體變元被量化的謂詞。二階謂詞:個體變元被量化,函數(shù)符號和謂詞符號也被量化。

P

xP(x)全稱命題:

xP(x)等價于P(a1)P(a2)…P(an)

特稱命題

xG(x)等價于P(a1)P(a2)…P(an)7/24/2023235.1.2謂詞公式(8)定義4:合取范式(ConjunctiveNormalForm)

設(shè)A為如下形式的謂詞公式:B1

B2

Bn其中Bi(i=1,2,…,n)形如L1

L2…

Lm,Lj(j=1,2,…,m)為原子公式或其否定,則A稱為合取范式。例(P(x)

Q(y))

(?P(x)Q(y)R(x,y))

(?Q(x)?R(x,y))就是一個合取范式7/24/2023245.1.2謂詞公式(9)定義5:析取范式(DisjunctiveNormalForm)設(shè)A為如下形式的謂詞公式:B1

B2…

Bn其中Bi(i=1,2,…,n)形如L1

L2

Lm,Lj(j=1,2,…,m)為原子公式或其否定,則A稱為析取范式。例(P(x)

?Q(y)

R(x,y))(?P(x)Q(y))(?P(x)R(x,y))就是一個析取范式7/24/2023255.1.2謂詞公式(10)謂詞公式的解釋

設(shè)D為謂詞公式P的個體域,若對P中的個體常量、函數(shù)和謂詞按如下規(guī)定賦值:(1)為每個個體常量指派D中的一個元素;(2)為每個n元函數(shù)指派一個從Dn到D的映射,其中Dn={(x1,x2,…,xn)/x1,x2,…,xn∈

D}(3)為每個n元謂詞指派一個從Dn到{F,T}的映射。則稱這些指派為公式P在D上的一個解釋。7/24/2023265.1.2謂詞公式(11)例:設(shè)個體域D={1,2},求公式A=xyP(x,y)在D上的解釋,并指出在每一種解釋下公式A的真值。解:公式里沒有個體常量和函數(shù),所以直接為謂詞指派真值,設(shè)為P(1,1)=TP(1,2)=FP(2,1)=TP(2,2)=F

這就是A在D上的一個解釋。在此解釋下:當(dāng)x=1時有y=1使P(x,y)的真值為T;當(dāng)x=2時有y=1使P(x,y)的真值為T;即對于D中的所有X都有y=1使P(x,y)的真值為T,所以在此解釋下公式A的真值為T。7/24/2023275.1.2謂詞公式(12)例:設(shè)個體域D={1,2},求公式A=xP(x)Q(f(x),b)在D上的解釋,并指出在每一種解釋下公式A的真值。解:為個體常量b指派D中的值:b=1為函數(shù)f(x)指派D中的值f(1)=2,f(2)=1對謂詞指派真值為:P(1)=F,P(2)=T,Q(1,1)=T,Q(2,1)=F

7/24/2023285.1.2謂詞公式(13)在此解釋下,當(dāng)x=1時有:

P(1)=F,Q(f(1),1)=Q(2,1)=F所以P(x)Q(f(x),b)為T。當(dāng)x=2時有P(2)=T,Q(f(2),1)=Q(1,1)=T所以P(x)Q(f(x),b)為T。即對個體域D中的所有x均有P(x)Q(f(x),b),所以公式B在此解釋下的真值為T。7/24/2023295.1.2謂詞公式(14)定義6:謂詞公式在個體域上的永真、永假、可滿足設(shè)P為謂詞公式,D為其個體域,對于D中的任一解釋I:(1)若P恒為真,則稱P在D上永真或是D上的永真式。(2)若P恒為假,則稱P在D上永假或是D上的永假式。(3)若至少有一個解釋,可是P為真,則稱P在D上是可滿足式。7/24/2023305.1.2謂詞公式(15)定義7:謂詞公式全個體域上的永真、永假、可滿足設(shè)P為謂詞公式,對于任何個體域:(1)若P都永真,則稱P為永真式。(2)若P都永假,則稱P為永假式。(3)若P都可滿足,則稱P為可滿足式。謂詞公式的真值與個體域及真值有關(guān),考慮到個體域的數(shù)目和個體域中元素數(shù)目無限的情形,所以要通過算法判斷一個謂詞公式永真是不可能的,所以稱一階謂詞邏輯是不可判定的。7/24/2023315.1.3謂詞邏輯中的形式演繹推理(1)自然演繹推理

利用一階謂詞推理規(guī)則的符號表示形式,可以把關(guān)于自然語言的邏輯推理問題,轉(zhuǎn)化為符號表達(dá)式的推演變換。這種推理十分類似于人們用自然語言推理的思維過程,因而稱為自然演繹推理。常用邏輯等價式常用邏輯蘊(yùn)含式

7/24/202332常用邏輯等價式(1)7/24/202333常用邏輯等價式(2)7/24/202334常用邏輯等價式(3)7/24/202335常用邏輯等價式(4)7/24/202336常用邏輯蘊(yùn)含式(1)7/24/202337常用邏輯蘊(yùn)含式(2)7/24/2023385.1.3謂詞邏輯中的形式演繹推理(2)例5.4設(shè)有前提:(1)凡是大學(xué)生都學(xué)過計算機(jī);(2)小王是大學(xué)生。試問:小王學(xué)過計算機(jī)嗎?解:令S(x):x是大學(xué)生M(x):x學(xué)過計算機(jī);a:小王上面命題用謂詞公式表示為:[前提][(1),US][前提][(2),(3),I3]我們進(jìn)行形式推理:M(a),即小王學(xué)過計算機(jī)。xA(x)=>A(y)y是個體域中任一確定元素(AB)A=>B7/24/2023395.1.3謂詞邏輯中的形式演繹推理(3)例5.5證明是和邏輯結(jié)果。證:[前提][(1),US][(2),US][前提][(3),(4),I4](AB)?B=>?A拒取式7/24/2023405.1.3謂詞邏輯中的形式演繹推理(4)例5.6證明

證:[前提][(1),US][(2),E24][(3),(5),I6][前提][(4),US][(1),UG]AB=>?B?A逆反律(AB)(BC)=>AB假言三段論A(y)=>xA(x)

全稱推廣規(guī)則7/24/2023415.2歸結(jié)演繹推理5.2.1子句集5.2.2命題邏輯中的歸結(jié)原理5.2.3替換與合一5.2.4謂詞邏輯中的歸結(jié)原理7/24/2023425.2.1子句集(1)定義1:原子謂詞公式及其否定稱為文字若干個文字的一個析取式稱為一個子句由r個文字組成的子句叫r-文字子句1-文字子句叫單元子句不含任何文字的子句稱為空子句,記為?或NIL。例如:?D(y)I(a)

PQ?R

?I(z)R(z)7/24/2023435.2.1子句集(2)定義2:對一個謂詞公式G,通過以下步驟所得的子句集S,稱為G的子句集(clauses)。

例5.7:x{yP(x,y)?y[Q(x,y)R(x,y)]}由第一步可得:x{?yP(x,y)?y[?Q(x,y)R(x,y)]}1、消蘊(yùn)含詞和等值詞

理論根據(jù):AB?ABAB(?AB)(?BA)蘊(yùn)含表達(dá)式7/24/2023445.2.1子句集(3)x{?yP(x,y)?y[?Q(x,y)R(x,y)]}

x{y?P(x,y)z[Q(x,z)?R(x,z)]}

3、適當(dāng)改名,使變量標(biāo)準(zhǔn)化 即:對于不同的約束,對應(yīng)于不同的變量2、移動否定詞作用范圍,使其僅作用于原子公式

理論根據(jù):?(?A)A?(AB)?A?B ?(AB)?A?B ?xP(x)x?P(x) ?xP(x)x?P

(x)雙重否定律摩根定律量詞轉(zhuǎn)換定律=>

x{y?P(x,y)y[Q(x,y)?R(x,y)]}7/24/2023455.2.1子句集(4)4、

消去存在量詞(Skolem化),同時進(jìn)行變元替換

原則:對于一個受存在量詞約束的變量,如果它

不受全稱量詞約束,則該變量用一個常量代替(這個常量叫Skolem常量),如果它受全稱量詞約束,則該變量用一個全稱量詞指導(dǎo)變元的函數(shù)代替(這個函數(shù)叫Skolem函數(shù))。

x{y?P(x,y)z[Q(x,z)?R(x,z)]}=>x{?P(x,f(x))[Q(x,g(x))?R(x,g(x))]}?P(x,f(x))[Q(x,g(x))?R(x,g(x))]5、消去所有全稱量詞。7/24/2023465.2.1子句集(5)

[?P(x,f(x))Q(x,g(x))][?P(x,f(x))?R(x,g(x))][?P(x,f(x))Q(x,g(x))][?P(y,f(y))?R(y,g(y))]7、適當(dāng)改名,使子句間無同名變元{?P(x,f(x))Q(x,g(x)),?P(y,f(y))?R(y,g(y))}8、消去合取詞,以子句為元素組成一個集合S6、化公式為合取范式理論依據(jù):A(BC)(AB)(AC)(AB)C(AC)(BC)?P(x,f(x))[Q(x,g(x))?R(x,g(x))]7/24/2023475.2.1子句集(6)

子句集:無量詞約束;(3,4,5)元素只是文字的析??;(1)否定符只作用于單個文字;(2)元素間默認(rèn)為合取。(6,7,8)化子句集的步驟:1、消去蘊(yùn)含詞和等值詞。2、使否定詞僅作用于原子公式。3、適當(dāng)改名使量詞間不含同名指導(dǎo)變元。4、消去存在量詞。5、消去全稱量詞。6、化公式為合取范式。7、適當(dāng)改名,使子句間無同名變元。8、消去合取詞,以子句為元素組成一個集合S。7/24/2023485.2.1子句集(7)練習(xí):用謂詞公式表示下述命題。已知前提:(1)自然數(shù)都是大于零的整數(shù)。(2)所有整數(shù)不是偶數(shù)就是奇數(shù)。(3)偶數(shù)除以2是整數(shù)。結(jié)論:所有自然數(shù)不是奇數(shù)就是一半為整數(shù)的數(shù)。化F1

F2F3

?G的子句集。

F1:x(N(x)GZ(x)I(x))F2:x(I(x)(E(x)O(x)))F3:x(E(x)I(s(x)))G:x(N(x)(I(s(x))O(x)))7/24/2023495.2.1子句集(8)解:F1F2F3?G的子句集為(1)?N(x)GZ(x)(2)?N(y)I(y)(3)?I(z)E(z)O(z)(4)?E(u)I(s(u))(5)N(a)(6)?O(a)(7)?I(s(a))7/24/2023505.2.1子句集(9)Skolem標(biāo)準(zhǔn)型在求子句集的過程中,消去存在量詞之后,把所有全稱量詞都依次移到式子的最左邊(或者把所有的量詞都依次移到式子最右邊,再消去存在量詞),再將右部的式子化為合取范式,這樣得到的式子就是Skolem標(biāo)準(zhǔn)型。x{y?P(x,y)z[Q(x,z)?R(x,z)]}=>x{?P(x,f(x))[Q(x,g(x))?R(x,g(x))]}=>x{[?P(x,f(x))Q(x,g(x))][?P(x,f(x))?R(x,g(x))]}{?P(x,f(x))Q(x,g(x)),?P(y,f(y))?R(y,g(y))}消去合取詞和全稱量詞,就得到了原公式的子句集7/24/2023515.2.1子句集(10)例5.8設(shè)消去存在量詞用a代替x用f(y,z)代替u用g(y,z,v)代替w得到G的Skolem標(biāo)準(zhǔn)型進(jìn)而得G的子句集為:

7/24/2023525.2.1子句集(11)

引入Skolem函數(shù),是由于存在量詞在全稱量詞的轄域內(nèi),其約束變元的取值完全依賴于全稱量詞的取值。Skolem反映了這種依賴關(guān)系。但Skolem標(biāo)準(zhǔn)型與原公式一般并不等價。

有公式:G=xP(x)它的Skolem標(biāo)準(zhǔn)型是G’=P(a)我們給出如下的解釋I:D={0,1},a/0,P(0)/F,P(1)/T在此解釋下,G=T,G’=F7/24/2023535.2.1子句集(12)定理1:謂詞公式G不可滿足當(dāng)且僅當(dāng)其子句集S不可滿足。定義3:子句集S是不可滿足的,當(dāng)且僅當(dāng)其全部子句的合取式是不可滿足的。7/24/2023545.2.2命題邏輯中的歸結(jié)原理(1)歸結(jié)原理的提出歸結(jié)原理(principleofresolution)又稱消解原理,1965年魯濱遜(J.A.Robinson)提出,從理論上解決了定理證明問題。歸結(jié)原理提出的是一種證明子句集不可滿足性,從而實(shí)現(xiàn)定理證明的一種理論及方法。7/24/2023555.2.2命題邏輯中的歸結(jié)原理(2)定義4設(shè)L為一個文字,則L與?L為互補(bǔ)文字。

定義5設(shè)C1,

C2是命題邏輯中的兩個子句,C1中有文字L1,C2中有文字L2,且L1與L2互補(bǔ),從C1、

C2中分別刪除L1、L2,再將剩余部分析取起來,記構(gòu)成的新子句為C12,則C12為C1、

C2的歸結(jié)式,C1、

C2稱為其歸結(jié)式的親本子句,稱L1、L2為消解基。例5.9設(shè),則C1、

C2的歸結(jié)式為:

7/24/2023565.2.2命題邏輯中的歸結(jié)原理(3)定理2歸結(jié)式是其親本子句的邏輯結(jié)果。證明:設(shè)C1=LC1’,C2=?LC2’其中C1’、C2’都是文字的析取式。則C1C2的邏輯結(jié)果為

C1=C1’L=?C1’→

LC2=?LC2’=L→

C2’由假言三段論得:

C1∧

C2=(?C1’→

L)∧(

L→

C2’)=>?C1’→

C2’=C1’C2’則C1

C2的歸結(jié)式為C1’C2’命題邏輯中的歸結(jié)原理:7/24/2023575.2.2命題邏輯中的歸結(jié)原理(4)例5.10用歸結(jié)原理驗證分離規(guī)則和拒取式

A∧(A→B)=>B(A→B)∧﹁B=>﹁A

A∧(A→B)=A∧(﹁A∨B)=>B(A→B)∧﹁B=(﹁A∨B)∧(﹁B)=>﹁A

7/24/2023585.2.2命題邏輯中的歸結(jié)原理(5)類似的可以驗證其他推理規(guī)則。這說明,歸結(jié)原理可以代替其他所有的推理規(guī)則,而且推理步驟比較機(jī)械,為機(jī)器推理提供了方便。由歸結(jié)原理可知:L∧?L=NIL另外我們知道:L∧?L=F(假),也就是

NILF7/24/2023595.2.2命題邏輯中的歸結(jié)原理(6)利用歸結(jié)原理證明命題公式的思路先求出要證明的命題公式的否定式的子句集S;然后對子句集S(一次或者多次)使用歸結(jié)原理;若在某一步推出了空子句,即推出了矛盾,則說明子句集S是不可滿足的,從而原否定式也是不可滿足的,進(jìn)而說明原公式是永真的。7/24/2023605.2.2命題邏輯中的歸結(jié)原理(7)推出空子句就說明子句集不可滿足,原因是:空子句就是F,推出空子句就是推出了F。歸結(jié)原理是正確的推理形式,由正確的推理形式推出了F,則說明前提不真,即歸結(jié)出空子句的兩個親本子句至少有一個為假。而這兩個親本子句如果都是原子句集S中不可滿足。如果這兩個親本子句不是或不全是S中的子句,那么它們必定是某次歸結(jié)的結(jié)果。同樣的道理向上回溯,一定會推出原子句集中至少有一個子句為假,從而說明S不可滿足。7/24/2023615.2.2命題邏輯中的歸結(jié)原理(8)推論設(shè)C1,

C2是子句集S的兩個子句,C12是它們的歸結(jié)式,則(1)若用C12來代替C1,

C2,得到新的子句集S1,則由S1不可滿足性可以推出原子句集S的不可滿足性。即(2)若用C12加入到S中,得到新的子句集S2,則S2與原S的同不可滿足。即S1的不可滿足性=>S不可滿足S2的不可滿足性<=>S不可滿足7/24/2023625.2.2命題邏輯中的歸結(jié)原理(9)例5.12設(shè)公理集:P,(PQ)R,(ST)Q,T求證:R化子句集: (PQ)R=>?(PQ)R=>?P?QR (ST)Q=>?(ST)Q=>(?S?T)Q=>(?SQ)(?TQ)=>{?SQ,?TQ}子句集: (1)P (2)?P?QR (3)?SQ (4)?TQ (5)T (6)?R(目標(biāo)求反)

7/24/2023635.2.2命題邏輯中的歸結(jié)原理(10)子句集: (1)P (2)?P?QR (3)?SQ (4)?TQ (5)T (6)?R(目標(biāo)求反)歸結(jié): (7)?P?Q(2,6) (8)?Q (1,7)(9)?T(4,8)(10)NIL(5,9)?P?QR?R?P?QP?Q?TQ?TTNIL7/24/2023645.2.2命題邏輯中的歸結(jié)原理(11)練習(xí):證明子句集{P?Q,?

P,Q}是不可滿足。7/24/2023655.2.3替換與合一(1)問題

在一階謂詞中應(yīng)用消解原理,無法直接找到互否文字的子句對例如:P(x)Q(z),?P(f(y))R(y)

P(x)Q(y),?P(a)R(z)解決方法

對個體變元做適當(dāng)替換例如:P(f(y))Q(z),?P(f(y))R(y)

P(a)Q(y),?P(a)R(y)7/24/2023665.2.3替換與合一(2)定義6一個替換(Substitution)是形如{t1/x1,t2/x2,…,tn/xn}的有限集合,其中t1,t2,…,tn是項,稱為替換的分子;x1,x2,…,xn是互不相同的個體變元,稱為替換的分母;ti,xi不同,xi不循環(huán)出現(xiàn)在tj中;ti/xi表示用ti替換xi。若其中t1,t2,…,tn是不含變元的項(稱為基項)時,該替換為基替換;沒有元素的替換稱為空替換,記作ε,表示不作任何替換。{a/x,g(a)/y,f(g(b))/z}就是一個替換{g(y)/x,f(x)/y}就不是一個替換,x與y出現(xiàn)了循環(huán)替換7/24/2023675.2.3替換與合一(3)

表達(dá)式:項、原子公式、文字、子句的統(tǒng)稱?;磉_(dá)式:沒有變元的表達(dá)式。子表達(dá)式:出現(xiàn)在表達(dá)式E中的表達(dá)式稱為E的子表達(dá)式。定義7設(shè)θ={t1/x1,t2/x2,…,tn/xn}是一個替換,E是一個表達(dá)式,對公式E實(shí)施替換θ,即把E中出現(xiàn)的個體變元xj都是tj的替換,記為Eθ,所得的結(jié)果稱為E在θ下的例(instance)。例如:若θ={a/x,f(b)/y,c/z},G=P(x,y,z)

Gθ=P(a,f(b),c)7/24/2023685.2.3替換與合一(4)定義8設(shè)θ={t1/x1,t2/x2,…,tn/xn},

λ=

{u1/y1,u2/y2,…,un/yn}是兩個替換,則將{t1λ

/x1,t2λ

/x2,…,tnλ

/xn,u1/y1,u2/y2,…,un/yn}中符合下列條件的元素刪除

(1)tiλ

/xi當(dāng)tiλ

xi

(2)ui/yi當(dāng)yi∈

{x1,…,xn}這樣得到的集合為θ與λ的復(fù)合或乘積,記為θ

。例:設(shè)θ={f(y)/x,z/y},λ={a/x,b/y,y/z}

{t1λ

/x1,t2λ

/x2,u1/y1,u2/y2,u3/yn}={f(b)/x,y/y,a/x,b/y,y/z}從而θ

?λ={f(b)/x,y/z}7/24/2023695.2.3替換與合一(5)定義9設(shè)S={F1,F2,…,Fn}

是一個原子謂詞公式集,若存在一個替換θ,可使F1θ

=F2θ=…=Fnθ,則稱θ為S的一個合一,稱S為可合一的。例:{P(x,f(y),B),P(z,f(B),B)}替換s={A/x,B/y,A/z}是一個合一,因為: P(x,f(y),B)s=P(A,f(B),B) P(z,f(B),B)s=P(A,f(B),B) 替換s={z/x,B/y}和替換s={x/z,B/y}也都是合一。一個公式的合一一般不唯一7/24/2023705.2.3替換與合一(6)定義10設(shè)σ是原子公式集S的一個合一,如果對S的任何一個合一

θ都存在一個替換λ,使得

θ=σ

?λ則稱σ為S的最一般合一(MostGeneralUnifier),簡稱MGU。一個公式集的MGU也是不唯一的。例:設(shè)S={P(u,y,g(y)),P(x,f(u),z)},S有一個最一般合一

σ={u/x,f(u)/y,g(f(u))/z}對S的任一合一,例如:

θ={a/x,f(a)/y,g(f(a))/z,a/u}存在一個替換

λ={a/u}使得θ=σ

?λ7/24/2023715.2.3替換與合一(7)定義11設(shè)S是一個非空的具有相同謂詞名的原子公式集,從S中各公式左邊的第一項開始,同時向右比較,直到發(fā)現(xiàn)第一個不都相同的項為止,用這些項的差異部分組成的集合就是S的一個差異集。例:設(shè)S={P(x,y,z),P(x,f(a),h(b))}根據(jù)上述差異集定義我們可以看出S有兩個差異集:D1={y,f(a)}D2={z,h(b)}7/24/2023725.2.3替換與合一(8)合一算法(Unificationalgorithm)Step1:置k=0,Sk=S,σk=ε;Step2:若Sk只含有一個謂詞公式,則算法停止,σk就是最一般合一;Step3:求Sk的差異集Dk;Step4:若中存在元素xk和tk,其中xk是變元,tk是項且xk不在tk中出現(xiàn),則置Sk+1=Sk{tk/

xk}σk+1=σk{tk/xk}

k=k+1然后轉(zhuǎn)Step2;Step5:算法停止,S的最一般合一不存在。7/24/2023735.2.3替換與合一(9)例:求公式集S={P(a,x,f(g(y))),P(z,h(z,u),f(u))}的最一般合一。解k=0;S0=S,σ0=ε,D0={a,z}σ1=σ0·{a/z}={a/z}S1=S0·{a/z}={P(a,x,f(g(y))),P(a,h(a,u),f(u))}k=1;D1={x,h(a,u)}σ2=σ1·{h(a,u)/x}={a/z,h(a,u)/x}S2=S1·{a/z,h(a,u)/x}={P(a,h(a,u),f(g(y))),P(a,h(a,u),f(u))}k=2;D2={g(y),u}σ3={a/z,h(a,u)/x,g(y),u}S3=S2·{g(y),u}={P(a,h(a,g(y)),f(g(y)))}S3單元素集,σ3為MGU。7/24/2023745.2.3替換與合一(10)例5.17判定S={P(x,x),P(y,f(y))}是否可合一?解k=0:S0=S,σ0=ε,S0不是單元素集,D0={x,y}σ1=σ0·{y/x}={y/x}S1=S0{y/x}={P(y,y),P(y,f(y))}k=1:

S1不是單元素集,D1={y,f(y)},由于變元y在項f(y)中出現(xiàn),所以算法停止,S不存在最一般合一。

7/24/2023755.2.3替換與合一(11)定理3(合一定理)S是非空有限可合一的公式集,則合一算法總在Step2停止,且最后的σk

一定是S的最一般合一(MGU)。對任一非空有限可合一的公式集,一定存在最一般合一,而且用合一算法一定能找到最一般合一。從合一算法可以看出,一個公式集S的最一般合一可能是不唯一的,因為如果差異集Dk={ak,bk},且ak和bk都是個體變元,則下面兩種選擇都是合適的:σk+1=σk·{bk/ak}或σk+1=σk·{ak/bk}7/24/2023765.2.4謂詞邏輯中的歸結(jié)原理(1)例:P(x)Q(y),?P(f(z))R(z) =>Q(y)R(z)定義12C1,C2為無相同變元的子句;L1,L2為其中的兩個文字,L1和?L2有最一般合一σ;C1,C2的二元?dú)w結(jié)式(二元消解式)為:

(C1

σ-{L1

σ})∪(

C2σ-{L2σ})其中C1,C2稱作歸結(jié)式的親本子句;L1,L2稱作消解文字。

7/24/2023775.2.4謂詞邏輯中的歸結(jié)原理(2)例5.18設(shè)C1=P(x)∨Q(x),C2=?P(a)∨R(y),求C1,C2的歸結(jié)式。解取L1=P(x),L2=P(a),則L1與L2的最一般合一σ={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的二元?dú)w結(jié)式。7/24/2023785.2.4謂詞邏輯中的歸結(jié)原理(3)

例5.19設(shè)C1=P(x,y)∨Q(a),C2=?Q(x)∨R(y),求C1,C2的歸結(jié)式。解由于C1,C2中都含有變元x,y,所以需先對其中一個進(jìn)行改名,方可歸結(jié)(歸結(jié)過程是顯然的,故從略)。還需說明的是,如果在參加歸結(jié)的子句內(nèi)部含有可合一的文字,則在進(jìn)行歸結(jié)之前,也應(yīng)對這些文字進(jìn)行合一,從而使子句達(dá)到最簡。7/24/2023795.2.4謂詞邏輯中的歸結(jié)原理(4)例如,設(shè)有兩個子句:C1=P(x)∨P(f(a))∨Q(x)C2=?P(y)∨R(b)可見,在C1,C2中有可合一的文字P(x)與P(f(a))取替換θ={f(a)/x}現(xiàn)在再用C1θ與C2進(jìn)行歸結(jié),從而得到C1與C2的歸結(jié)式Q(f(a))∨R(b)則得C1θ=P(f(a))∨Q(f(a))7/24/2023805.2.4謂詞邏輯中的歸結(jié)原理(5)例5.20:C=P(x)P(f(y))?Q(x),σ={f((y)/x}

Cσ=P(f(y))?Q(x)是C的因子。定義13子句C中,兩個或兩個以上的文字有一個最一般合一σ,則稱Cσ為C的因子,若Cσ

為單元子句,則Cσ稱為C的單因子。7/24/2023815.2.4謂詞邏輯中的歸結(jié)原理(6)定義14子句的C1,C2消解式,是下列二元消解式之一:

(1)C1和C2的二元消解式;(2)C1和C2的因子的二元消解式;(3)C1因子和C2的二元消解式;(4)C1的因子和C2的因子的二元消解式。7/24/2023825.2.4謂詞邏輯中的歸結(jié)原理(7)定理4謂詞邏輯中的消解(歸結(jié))式是它的親本子句的邏輯結(jié)果。謂詞邏輯的推理規(guī)則:

C1

C2

=>(C1

σ-{L1

σ})∪(

C2σ-{L2σ})其中C1

,C2

是兩個無相同變元的子句,L1,L2分別是C1

,C2中的文字σ為

L1和L2的最一般合一。這個規(guī)則稱為謂詞邏輯中的消解原理(或歸結(jié)原理)。7/24/2023835.2.4謂詞邏輯中的歸結(jié)原理(8)例5.21求證G是A1和A2的邏輯結(jié)果。A1:(x)(P(x)(Q(x)R(x)))

A2

:(x)(P(x)S(x))G:(x)(S(x)R(x))證:利用歸結(jié)反演法,先證明A1A2?G是不可滿足的。求子句集:

(1)?P(x)Q(x)(2)?P(y)R(y)(3)P(a)(4)S(a)(5)?S(z)?R(z)(?G)A2A1S7/24/2023845.2.4謂詞邏輯中的歸結(jié)原理(9)應(yīng)用消解原理,得:(6)R(a)[(2),(3),σ1={a/y}](7)?R(a)[(4),(5),σ2={a/z}](8)Nil[(6),(7)]所以S是不可滿足的,從而G是A1和A2的邏輯結(jié)果。子句集S

(1)?P(x)Q(x)(2)?P(y)R(y)(3)P(a)(4)S(a)(5)?S(z)?R(z)7/24/2023855.2.4謂詞邏輯中的歸結(jié)原理(10)例5.22設(shè)已知:(1)能閱讀者是識字的;(2)海豚不識字;(3)有些海豚是很聰明的。試證明:有些聰明者并不能閱讀。證首先定義如下謂詞:R(x):x能閱讀。L(x):x能識字。I(x):x是聰明的。D(x):x是海豚。將上述各語句翻譯成謂詞公式:(1)(x)(R(x)L(x))(2)(x)(D(x)?L(x))已知條件(3)(x)(D(x)I(x))(4)(x)(I(x)?R(x))需證結(jié)論7/24/2023865.2.4謂詞邏輯中的歸結(jié)原理(11)用歸結(jié)反演法來證明,求題設(shè)與結(jié)論否定的子句集,得:

(1)?

R(x)L(x)(2)?

D(y)?L(y)(改名)(3)D(a)(4)I(a)(5)?I(z)R(z)歸結(jié)得:(6)R(a)[(5),(4),{a/z}](7)L(a)[(6),(1),{a/x}](8)?D(a)[(7),(2),{a/y}](9)Nil[(8),(3)]?I(z)R(z)R(a)L(a)?D(a)NilI(a)?R(x)L(x)?D(y)L(y)D(a)7/24/2023875.2.4謂詞邏輯中的歸結(jié)原理(12)定理5如果子句集S是不可滿足的,那么必存在一個由S推出空子句的消解序列。7/24/2023885.2.4謂詞邏輯中的歸結(jié)原理(13)練習(xí)設(shè)已知:(1)自然數(shù)都是大于零的整數(shù);(2)所有整數(shù)不是偶數(shù)就是奇數(shù);(3)偶數(shù)除以2是整數(shù)。試證明:所有自然數(shù)不是奇數(shù)就是其一半為整數(shù)的數(shù)。證首先定義如下謂詞:N(x):x是自然數(shù)。I(x):x是整數(shù)。E(x):x是偶數(shù)。O(x):x是奇數(shù)。GZ(x):x大于零。s(x):x除以2。將上述各語句翻譯成謂詞公式:

F1:x(N(x)GZ(x)I(x))

F2:x(I(x)(E(x)O(x)))

F3:x(E(x)I(s(x)))

G:

x(N(x)(I(s(x))O(x)))

7/24/2023895.2.4謂詞邏輯中的歸結(jié)原理(14)利用歸結(jié)反演法,先證明F1F2F3?G是不可滿足的。F1F2F3?G的子句集為(1)?N(x)GZ(x)(2)?N(y)I(y)(4)?E(u)I(s(u))(3)?I(z)E(z)O(z)(5)N(a)(6)?O(a)(7)?I(s(a))7/24/2023905.3應(yīng)用歸結(jié)原理求取問題答案(1)例5.23已知:(1)如果x和y是同班同學(xué),則x的老師也是y的老師。(2)王先生是小李的老師。(3)小李和小張是同班同學(xué)。問:小張的老師是誰?解首先定義如下謂詞:

T(x,y)表示x是y的老師

C(x,y)表示x與y是同班同學(xué)。

已知條件可以表示成如下謂詞公式:F1:xyz(C(x,y)T(z,x)T(z,y))F2:T(Wang,Li)F3:C(Li,Zhang)

7/24/2023915.3應(yīng)用歸結(jié)原理求取問題答案(2)

為了得到答案,首先要先證明小張的老師是存在的。即證明:G:xT(x,Zhang)

(1)?C(x,y)?T(z,x)T(z,y)(2)T(Wang,Li)(3)C(Li,Zhang)(4)?T(u,Zhang)求F1F2F3?

G的子句集:F1:xyz(C(x,y)T(z,x)T(z,y))F2:T(Wang,Li)F3:C(Li,Zhang)

7/24/2023925.3應(yīng)用歸結(jié)原理求取問題答案(3)歸結(jié)演繹得:(5)?C(Li,y)T(Wang,y)[(1),(2),{Wang/z,Li/x}](6)?C(Li,Zhang)[(4),(5),{Wang/u,Zhang/y}](7)Nil[(3),(6)]這說明小張的老師確實(shí)是存在的。

(1)?C(x,y)?T(z,x)T(z,y)(2)T(Wang,Li)(3)C(Li,Zhang)(4)?T(u,Zhang)7/24/2023935.3應(yīng)用歸結(jié)原理求取問題答案(4)

為了求取答案,給原來的子句增加一個輔助謂詞ANS(u),得到:(4)'?T(u,Zhang)ANS(u)

原來的子句集變?yōu)椋?1)?C(x,y)?T(z,x)T(z,y)(2)T(Zhang,Li)(3)C(Li,Zhang)(4)'?T(u,Zhang)ANS(u)重新歸結(jié)演繹得:(5)'?C(Li,y)T(Wang,y)[(1),(2),{Wang/z,Li/x}](6)'?C(Li,Zhang)ANS(u)

[(4)',(5)

',{Wang/u,Zhang/y}](7)'ANS(Wang)[(3),(6)']這說明小張的老師存在且求得小張的老師是王先生。7/24/2023945.3應(yīng)用歸結(jié)原理求取問題答案(5)應(yīng)用歸結(jié)原理求取問題答案(方法思路)(1)先為待求解的問題找一個合適的求證目標(biāo)謂詞;(2)再增配(以析取形式)一個輔助謂詞,該謂詞的變元必須與對應(yīng)目標(biāo)謂詞中的變元完全一致;(3)進(jìn)行歸結(jié);(4)當(dāng)歸結(jié)是剛好只剩下輔助謂詞時,輔助謂詞中原變元位置上的項就是所求的結(jié)果。說明:其中輔助謂詞是一個形式謂詞,其作用僅是提取問題的答案。有時就用需求證的目標(biāo)謂詞。7/24/2023955.3應(yīng)用歸結(jié)原理求取問題答案(6)例5.24已知:(1)如果x是y的父親,y又是z的父親,則x是z的祖父。(2)老李是大李的父親。(3)大李是小李父親。問:上述人員誰和誰是祖孫關(guān)系?解首先定義如下謂詞:G(x,y)表示x是y的祖父。F(x,y)表示x與y是父親。

已知條件可以表示成如下謂詞公式:F1:xyz(F(x,y)F(y,z)G(x,z))F2:F(Lao,Da)F3:F(Da,Xiao)

7/24/2023965.3應(yīng)用歸結(jié)原理求取問題答案(7)

并求其子句集如下:

(1)?F(x,y)?F(y,z)G(x,z)(2)F(Lao,Da)(3)F(Da,Xiao)

設(shè)求證的公式為:G:x

yG(x,y)(既存在x和y,x是y的祖父)

把其否定化為子句形式再析取一個輔助謂詞GA(u,v)(4)?G(u,v)

GA(u,v)

已知條件可以表示成如下謂詞公式:F1:xyz(F(x,y)F(y,z)G(x,z))F2:F(Lao,Da)F3:F(Da,Xiao)

7/24/2023975.3應(yīng)用歸結(jié)原理求取問題答案(8)

把其否定化為子句形式再析取一個輔助謂詞GA(u,v)(1)?F(x,y)?F(y,z)G(x,z)(2)F(Lao,Da)(3)F(Da,Xiao)

(4)?G(u,v)

GA(u,v)

對上式進(jìn)行歸結(jié):(5)?F(Da,z)

G(Lao,z)[(1),(2),{Lao/x,Da/y}]

(6)G(Lao,Xiao)

[(3),(5),{Xiao/x}](7)GA(Lao,Xiao)[(4),(6),{Lao/u,Xiao/v}]所以上述人員中,老李是小李的祖父。7/24/2023985.3應(yīng)用歸結(jié)原理求取問題答案(9)練習(xí)1:已知如下事實(shí):(1)小李只喜歡較容易的課程;(2)工程類課程是較難的;(3)PR系的所有課程都是較容易的。(4)PR150是PR系的一門課程應(yīng)用歸結(jié)演繹推理回答問題:小李喜歡什么課程?

7/24/2023995.3應(yīng)用歸結(jié)原理求取問題答案(10)練習(xí)2:設(shè)A、B、C中有人從來不說真話,也有人從來不說謊話,某人向這三人分別同時提出一個問題:誰是說謊者?A答:“B和C都是說謊者”;B答:“A和C都是說謊者”;C答:“A和B中至少有一個人說謊”。用歸結(jié)原理求誰是老實(shí)人,誰是說謊者?7/24/20231005.4歸結(jié)策略5.4.1問題的提出5.4.2幾種常用的歸結(jié)策略5.4.3歸結(jié)策略的類型7/24/20231015.4.1問題的提出(1)研究歸結(jié)原理的目的是實(shí)現(xiàn)機(jī)器推理用歸結(jié)原理實(shí)現(xiàn)機(jī)器推理的一般性算法

Step1將子句集S置入CLAUSES表中;Step2若空子句NIL在CLAUSES中,則歸結(jié)成功,結(jié)束。Step3若CLAUSES表中存在可歸結(jié)的子句對,則歸結(jié)之,并將歸結(jié)式并入CLAUSES表中,轉(zhuǎn)Step2;Step4歸結(jié)失敗,退出。Step3中子句對進(jìn)行歸結(jié)的順序怎么確定

最簡單的方法是采用窮舉式地進(jìn)行歸結(jié)。7/24/20231025.4.1問題的提出(2)水平浸透法具體作法

第一輪歸結(jié)先讓CLAUSES表(原子句集S)中的子句兩兩見面進(jìn)行歸結(jié),將產(chǎn)生的歸結(jié)集合記為S1,再將S1并入CLAUSES中,得到CLAUSES=S∪S1;再一輪歸結(jié)時,又讓S∪S1∪S2與S2中的子句進(jìn)行歸結(jié)……如此進(jìn)行,知道某一個Sk中出現(xiàn)空子句為止。下一輪歸結(jié)讓新的CLAUSES表(S∪S1)中的子句與S1中的子句互相見面進(jìn)行歸結(jié),并把產(chǎn)生的歸結(jié)式集合記為S2,再將S2并入CLAUSES中;7/24/20231035.4.1問題的提出(3)S:(1)PQ(2)?PQ(3)P?Q(4)?P?QS1:(5)Q[(1),(2)](6)P[(1),(3)](7)Q?Q[(1),(4)](8)?PP[(1),(4)](9)Q?Q[(2),(3)](10)?PP[(2),(3)](11)?P[(2),(4)](12)?Q[(3),(4)]S2:(13)PQ[(1),(7)](14)PQ[(1),(8)](15)PQ[(1),(9)](16)PQ[(1),(10)](17)Q

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

最新文檔

評論

0/150

提交評論