《歸結(jié)演繹推理》PPT課件

《《歸結(jié)演繹推理》PPT課件》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在教育資源-天天文庫。

1、1第4章自動推理2第4章自動推理4.1引言4.2自然演繹推理4.3歸結(jié)演繹推理-134.3歸結(jié)演繹推理-14歸結(jié)證明過程是一種反駁程序，即：不是證明一個公式是有效的(valid)，而是證明公式之非是不可滿足的(dissatisfiable)。這完全是為了方便，并且不失一般性。埃爾布朗(Herbrand)(也稱海明倫)提出的埃爾布朗論域和埃爾布朗定理為自動定理證明奠定了理論基礎(chǔ)。魯賓遜(Robinson)原理使定理證明的機械化變?yōu)楝F(xiàn)實。4.3歸結(jié)演繹推理-15若欲證明前提條件P可推導(dǎo)出結(jié)論Q，即證明永真，該問題的證明等價

2、于證明永假，即是不可滿足的。4.3歸結(jié)演繹推理-16由于謂詞邏輯是命題邏輯的推廣，命題邏輯中的基本等價式和推理規(guī)則在謂詞邏輯仍可沿用。但由于謂詞邏輯中引入了變量及量詞，須再增加一些與變量、量詞有關(guān)的一些定理和規(guī)則，現(xiàn)一并歸納于下:4.3.1Skolem標(biāo)準(zhǔn)型7雙重否定律(doublenegationlaw):┓(┓P(x))≡P(x)德·摩根定律(Mogenlaw):┓(P(x)∨Q(x))≡┓P(x)∧┓Q(x)┓(P(x)∧Q(x))≡┓P(x)∨┓Q(x)1、謂詞演算的基本等價式8逆否律(inverse-nega

3、tionlaw):P(x)→Q(x)≡┓Q(x)→┓P(x)分配律(assignmentlaw):P(x)∧(Q(x)∨R(x))≡(P(x)∧Q(x))∨(P(x)∧R(x))P(x)∨(Q(x)∧R(x))≡(P(x)∨Q(x))∧(P(x)∨R(x))1、謂詞演算的基本等價式9結(jié)合律(associationlaw):（P(x)∧Q(x))∧R(x)≡P(x)∧(Q(x)∧R(x))（P(x)∨Q(x))∨R(x)≡P(x)∨(Q(x)∨R(x))蘊含等價式(implicationlaw):P(x)→Q(x)≡┓P

4、(x)∨Q(x)1、謂詞演算的基本等價式10易名規(guī)則(renamelaw):?xP(x)∨?xQ(x)≡?xP(x)∨?yQ(y)量詞轉(zhuǎn)換律(quantifiertransformlaw):┓?xP(x)≡?x┓P(x)┓?xP(x)≡?x┓P(x)1、謂詞演算的基本等價式11量詞分配律(quantifierassignmentlaw):?x(P(x)∨Q(x))≡?xP(x)∨?xQ(x)?x(P(x)∧Q(x))≡?xP(x)∧?xQ(x)?x(P→Q(x))≡P→?xQ(x)?x(P→Q(x))≡P→?xQ(x)

5、1、謂詞演算的基本等價式12量詞交換律(quantifiercommutativelaw):?x?y(P(x,y))≡?y?x(P(x,y))?x?y(P(x,y))≡?y?x(P(x,y))?x?y(P(x,y))??y?x(P(x,y))?x?y(P(x,y))??y?x(P(x,y))1、謂詞演算的基本等價式13量詞轄域變換等價式:?xP(x)∨Q≡?x(P(x)∨Q)?xP(x)∧Q≡?x(P(x)∨Q)?xP(x)∧Q≡?x(P(x)∨Q)?xP(x)∧Q≡?x(P(x)∨Q)Q中不含變量1、謂詞演算的基本等

6、價式14全稱量詞消去規(guī)則:?xP(x)≡P(y)全稱量詞引入規(guī)則:P(y)≡?xP(x)存在量詞消去規(guī)則:?xQ(x)≡Q(c)(c為常量)存在量詞引人規(guī)則:Q(c)≡?xQ(x)2、量詞消去及引入規(guī)則15有限域量詞消去規(guī)則:設(shè)有限個體域為D?d1，d2，……dn?xP(x)≡P(d1)∧P(d2)，……∧P(dn)?xQ(x)≡Q(d1)∨Q(d2)，……∨Q(dn)2、量詞消去及引入規(guī)則163、謂詞邏輯中的范式同一個命題或謂詞公式可以用不同的命題或謂詞公式形式來表達，這些公式形式之間是相互等值的。為了把這些公式規(guī)范

7、化，下面討論公式范式問題。所謂范式就是公式的標(biāo)準(zhǔn)形式，公式往往可以轉(zhuǎn)換為和它等價的范式，以便對它們做一般性的處理。方法是：對給定公式中的某子公式用與它“等價”的一個公式來代替，并且重復(fù)該過程直到得出所需要的形式為止。下面給出一些定義。17范式中的一些定義:定義4.1文字(literal)是原子或原子之非。定義4.2公式G，當(dāng)且僅當(dāng)G有形式G1∧…∧Gn(n>=1)其中每個Gi都是文字的析取式。則G稱為合取范式(conjunctivenormalform)3、謂詞邏輯中的范式18定義4.3公式G稱為析取范式(disjun

8、ctivenormalform)，邏輯公式的標(biāo)準(zhǔn)化(或規(guī)范化)，它是合取子句的析取.當(dāng)且僅當(dāng)G有形式G1∨…∨Gn(n>=1)其中每個Gi都是文字的合取式。例如:在命題邏輯中，若P、Q、R是原子，則P、Q、R、┓P、┓Q、┓R都是文字。(P∨┓Q∨R)∧(┓P∨Q)是合取范式。(┓P∧Q)∨(P∧┓Q∧┓R)是析取范式。3、謂詞邏