【文章內(nèi)容簡介】 變元不同 集合形式 沒有蘊含詞、等值詞 2022/2/16 51 (7) = ?x {? y 172。 P(x， y) ? ? z[Q(x,z) ? 172。 R(x,z)]} 適當(dāng)改名，使變量標(biāo)準(zhǔn)化 即：對于不同的約束，對應(yīng)于不同的變量 ?x {? y 172。 P(x， y) ? ? y [Q(x,y) ? 172。 R(x,y)]} 問題 :不同轄域的相同變元對應(yīng)的約束相同嗎 ? 2022/2/16 52 (8) 消去存在量詞 (Skolem化） ,同時進行變元替換 原則： ① 若該存在量詞 不在任何 全稱量詞 的轄域內(nèi)， 則 用一 個 常量符號 代替該存在量詞轄域內(nèi)的相應(yīng)約束變元， 這個常量叫 Skolem常量 ； ② 若該存在量詞 在 全稱量詞 的轄域內(nèi)， 則 用這些全 稱量詞指導(dǎo)變元的一個 函數(shù) 代替該存在量詞轄域 內(nèi)的相應(yīng)約束變元，這樣的函數(shù)稱為 Skolem函數(shù) 。 理論依據(jù)： ? xA（ x） =A（ y） y是個體域中某一確定的元素。 存在指定規(guī)則 2022/2/16 53 (9) 問題 :為什么受全稱量詞約束的要用 Skolem函數(shù)替換 ? 而不能用常量替換？ ?x ? yM（ y， x）： 對任意一個人 x，都存在一個 y， y是 x的媽媽。 若去掉存在量詞用常量 a代替 y，則變?yōu)椋? ?x M（ a， x）： a是所有人的媽媽。 實際上，引入 Skolem函數(shù)，是由于存在量詞在全稱量詞 的轄域之內(nèi)，其約束變元的取值完全依賴于全稱變量的 取值。而 Skolem函數(shù)反映了這種依賴關(guān)系。 2022/2/16 54 (10) ?x {? y 172。 P(x， y) ? ? z[Q(x,z) ? 172。 R(x,z)]} = ?x {172。 P(x， f(x)) ? [Q(x， g(x)) ? 172。 R(x， g(x))]} = 172。 P(x， f(x)) ? [Q(x,g(x)) ? 172。 R(x,g(x))] 消去所有全稱量詞。 理論依據(jù)： ? xA（ x） =A（ y） y是個體域中任一確定的元素。 全稱指定規(guī)則 2022/2/16 55 (11) ? 子句集的特征 “172。”作用原子謂詞 沒有量詞 (? 、 ? ) 合取范式 元素之間變元不同 集合形式 沒有蘊含詞、等值詞 2022/2/16 56 (12) = [172。 P(x， f(x)) ? Q(x,g(x))] ? [172。 P(x， f(x)) ? 172。 R(x,g(x))] 化公式為合取范式 理論依據(jù)： A?（ B ? C） （ A ? B） ? （ A ?C） （ A ? B ） ? C （ A ? C） ? （ B ?C） ??172。 P(x， f(x)) ? [Q(x,g(x)) ? 172。 R(x,g(x))] 分配律 2022/2/16 57 (13) ? 子句集的特征 “172?！弊饔迷又^詞 沒有量詞 (? 、 ? ) 合取范式 元素之間變元不同 集合形式 沒有蘊含詞、等值詞 2022/2/16 58 (14) =[172。 P(x， f(x)) ? Q(x,g(x))] ? [172。 P(y， f(y)) ? 172。 R(y,g(y))] 適當(dāng)改名，使子句間無同名變元 ={172。 P(x， f(x)) ? Q(x,g(x)) , 172。 P(y， f(y)) ? 172。 R(y,g(y))} 消去合取詞，以子句為元素組成一個集合 S = 172。 P(x， f(x)) ? [Q(x,g(x)) ? 172。 R(x,g(x))] 2022/2/16 59 子句集 小結(jié) 消去蘊含詞和等值詞 使否定詞僅作用于原子公式 使量詞間不含同名指導(dǎo)變元 消去存在量詞 消去全稱量詞 化公式為合取范式 子句間無同名變元 組成一個集合 “172?！弊饔迷又^詞 沒有量詞 (? 、 ? ) 合取范式 元素之間變元不同 集合形式 沒有蘊含詞、等值詞 蘊含等價式 雙重否定律、 摩根定律、 量詞轉(zhuǎn)換律 存在指定、 依賴關(guān)系 全稱指定 分配律 2022/2/16 60 子句集 練習(xí)（ 1） 練習(xí)：用謂詞公式表示下述命題。 已知前提： （ 1）自然數(shù)都是大于零的整數(shù)。 （ 2）所有整數(shù)不是偶數(shù)就是奇數(shù)。 （ 3）偶數(shù)除以 2是整數(shù)。 結(jié)論：所有自然數(shù)不是奇數(shù)就是除以 2為整數(shù)的數(shù)。 化 F1 ? F2 ? F3 ? 172。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))) 2022/2/16 61 子句集 練習(xí)（ 2） F1: ?x(N(x)?GZ(x)?I(x)) 由 (1)得 ?x(172。N(x)?(GZ(x)?I(x))) ?x((172。N(x)?I(x))?(172。N(x)?GZ(x))) 由 (5)得 (172。N(x)?I(x))?(172。N(x)?GZ(x)) 由 (7)得 (172。N(x)?I(x))?(172。N(y)?GZ(y)) 由 (8)得 {172。N(x)?I(x),172。N(y)?GZ(y)} F2: ?x(I(x)?(E(x)?O(x))) 由 (1)得 ?x(172。I(x)?(E(x)?O(x))) 由 (5)得 172。I(z)?E(z)?O(z) 由 (8)得 {172。I(z)?E(z)?O(z)} 2022/2/16 62 子句集 練習(xí)（ 3） F3: ?x(E(x)?I(s(x))) 由 (1)得 ?x(172。E(x)?I(s(x))) 由 (5)得 172。E(x)?I(s(x)) 由 (8)得 {172。E(u)?I(s(u))} 172。G: 172。?x(N(x)?(I(s(x))?O(x))) 由 (1)得 172。?x(172。N(x)?(I(s(x))?O(x))) 由 (2)得 ?x172。(172。N(x)?(I(s(x))?O(x))) ?x(N(x)?172。I(s(x))?172。 O(x)) 由 (4)得 N(a)?172。I(s(a))?172。 O(a) 由 (8)得 {N(a),172。I(s(a)),172。 O(a)} 2022/2/16 63 子句集 練習(xí)（ 4） 解： F1?F2?F3?172。G的子句集為 （ 1） 172。N(x) ? GZ(x) （ 2） 172。N(y) ? I(y) （ 3） 172。I(z) ? E(z) ?O(z) （ 4） 172。E(u) ? I(s(u)) （ 5） N(a) （ 6） 172。O(a) （ 7） 172。I(s(a)) 2022/2/16 64 子句集 練習(xí)應(yīng)用歸結(jié)原理證明定理 （ 1） 172。N(x) ? GZ(x) （ 2） 172。N(y) ? I(y) （ 3） 172。I(z) ? E(z) ?O(z) （ 4） 172。E(u) ? I(s(u)) （ 5） N(a) （ 6） 172。I(s(a)) （ 7） 172。O(a) （ 8） 172。E(a) [4,6,{a/u}] （ 9） 172。I(a)?E(a) [3,7,{a/z}] （ 10） 172。I(a) [8,9] （ 11） 172。N(a) [2,10] （ 12） □ [5,11] 2022/2/16 65 子句集 (18) Skolem標(biāo)準(zhǔn)型 在求子句集的過程中，消去存在量詞 之后，把所有 全稱量詞 都依次移到式子的最左邊（或者 把所有的量詞都依次移到式子最左邊，再消去存在量 詞），再將右部的式子化為合取范式，這樣得到的式 子就是原公式的 Skolem標(biāo)準(zhǔn)型。 ?x {? y 172。 P(x,y) ? ? z[Q(x,z) ? 172。 R(x,z)]} =?x {172。 P(x,f(x)) ? [Q(x,g(x)) ? 172。 R(x,g(x))]} =?x {[ 172。 P(x,f(x)) ? Q(x,g(x)) ] ? [ 172。 P(x,f(x)) ? 172。 R(x,g(x)) ] } {172。 P(x， f(x)) ? Q(x,g(x)) , 172。 P(y， f(y)) ? 172。 R(y,g(y))} 消去合取詞和全稱量詞，就得到了原公式的子句集 2022/2/16 66 子句集 (19) 例 ))w,v,u(Q)z,y,x(P(wvuzyxG ?????????消去存在量詞 用 a 代替 x 用 f(y,z) 代替 u 用 g(y,z,v)代替 w 得到 G的 Skolem標(biāo)準(zhǔn)型 )),(,v),((),(( vzygzyfQzyaPvzy ?????進而得 G的子句集為： ))}v,z,y(g,x),z,y(f(Q),z,y,a(P{ ?一個謂詞公式的子句集也可以通過求 前束范式 （如果謂詞公式中一切量詞都位于該公式最左邊，不含否定詞，且量詞的轄域都延伸到公式末端），再求 Skolem標(biāo)準(zhǔn)型而得到。 ))},(,),((),({ wvugwvufQzya ?2022/2/16 67 子句集 (20) 引入 Skolem函數(shù)，是由于存在量詞在全稱量詞的轄 域內(nèi)，其約束變元的取值完全依賴于全稱量詞的取值。 Skolem函數(shù)反映了這種依賴關(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’ ＝ F 2022/2/16 68 子句集 (21) 定理 1：謂詞公式 G不可滿足當(dāng)且僅當(dāng)其子句集 S不可滿足 定義 3：子句集 S是不可滿足的，當(dāng)且僅當(dāng)其全部子句的 合取式是不可滿足的。 謂詞公式正確性證明 謂詞公式否定式不可滿足性證明 謂詞公式對應(yīng)子句集的不可滿足性證明 2022/2/16 69 命題邏輯中的歸結(jié)原理 (1) ? 歸結(jié)原理的提出 歸結(jié)原理 (principle of resolution)又稱消解原理 ,1965年魯濱遜（ ）提出，從理論上解決了定理證明問題。歸結(jié)原理提出的是一種證明子句集不可滿足性，從而實現(xiàn)定理證明的一種理論及方法。 ? 歸結(jié)原理的基本原理是采用反證法（反演推理方法） ? 歸結(jié)算法是一節(jié)謂詞邏輯中的半可判定算法， ? 對一階邏輯中任意恒真公式使用歸結(jié)原理，總可以在有限步內(nèi)給以判定（證明其為永真） ? 對不知該公式是否為恒真時，使用歸結(jié)原理得不到任何結(jié)論 2022/2/16 70 命題邏輯中的歸結(jié)原理 (2) 定義 4 設(shè) L為一個文字，則 L與 172。L為 互補文字 。 定義 5 設(shè) C C2是命題邏輯中的兩個子句， C1中有文字 L C2中有文字 L且 L1與 L2互補， 從 C C2中分別刪除 L L2 ，再將剩余部分析 取起來，構(gòu)成的新子句為 C12，則 C12為 C C2的 歸結(jié)式 ， C C2稱為其歸結(jié)式的 親本子句 ，稱 L1 、 L2 為 消解基 。 例 設(shè) ，則 C1 、 C2的歸結(jié)式為： SQC,RQPC ??????? 21RSPC ????122022/2/16 71 命題邏輯中的歸結(jié)原理 (3) 定理 2 歸結(jié)式是其親本子句的邏輯結(jié)果。 證明：設(shè) C1=L?C1’ ， C2 = 172。 L ? C2’ 其中 C1’ 、 C2’ 都是文字的析取式。 C1 、 C2的歸結(jié)式為 C1’ ? C2’ C1 、 C2的邏輯結(jié)果為： C1