【正文】 元素集 ， σ3為 MGU。 2022/2/16 91 替換與合一 (10) 例 判定 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)｝，由于變?cè)?y在項(xiàng)f(y)中出現(xiàn)，所以算法停止， S不存在最一般合一。 2022/2/16 92 替換與合一 (11) 定理 3 (合一定理 ) S是非空有限可合一的公式集，則合一算法總在 Step2停止，且最后的 σ k即是 S的最一般合一（ MGU）。 對(duì)任一非空有限可合一的公式集，一定存在最一般合 一，而且用合一算法一定能找到最一般合一，即算法終止在第 2步時(shí)最后的合一 σk 從合一算法可以看出，一個(gè)公式集 S的最一般合一可能是不唯一的。如果差異集 Dk=｛ ak,bk｝，且 ak和 bk都是個(gè)體變?cè)瑒t下面兩種選擇都是合適的： σ k+1=σ k｛ bk/ak｝或 σ k+1=σ k｛ ak/bk｝ 2022/2/16 93 謂詞邏輯中的歸結(jié)原理 (1) 例 ： P(x)?Q(y), 172。P(f(z))?R(z) = Q(y)?R(z) 定義 12 設(shè) C1， C2為無相同變?cè)淖泳洌? L1， L2為其中的兩個(gè)文字 。 L1和 172。L2有最一般合一 σ ； 則 C1， C2的 二元?dú)w結(jié)式（二元消解式） 為： （ C1σ － {L1σ }） ∪ （ C2σ － {L2σ }） 其中 C1， C2稱作歸結(jié)式的 親本子句 ； L1， L2稱作 消解文字 。 2022/2/16 94 謂詞邏輯中的歸結(jié)原理 (2) 例 設(shè) C1=P(x)∨ Q(x),C2= 172。 P(a)∨ R(y)，求 C1,C2的歸結(jié)式。 解 取 L1=P(x), 172。 L2=P(a), L1與 172。 L2 的 MGUσ={a/x｝ (C1σ｛ L1σ｝ )∪ (C2σ ｛ L2σ｝ ) =({P(a),Q(a)}{P(a)})∪ ({172。 P(a),R(y)}{172。 P(a)}) ={Q(a),R(y)} =Q(a)∨ R(y) 所以， Q(a)∨ R(y)是 C1和 C2的二元?dú)w結(jié)式。 2022/2/16 95 (3) 例 設(shè) C1=P(x,y)∨ Q(a),C2= 172。 Q(x)∨ R(y),求 C1,C2的歸結(jié)式。 解 由于 C1,C2中都含有變?cè)?x,y，所以需先對(duì)其中一個(gè)進(jìn)行改名 ,方可歸結(jié)。 如果在參加歸結(jié)的子句內(nèi)部含有可合一的文字，則在進(jìn)行歸結(jié)之前，也應(yīng)對(duì)這些文字進(jìn)行合一，從而使子句達(dá)到最簡(jiǎn)。 歸結(jié)過程需要注意兩點(diǎn)： 兩個(gè)子句含有相同的變?cè)枰獙?duì)其中一個(gè)進(jìn)行改名 2022/2/16 96 (4) 例如，設(shè)有兩個(gè)子句： C1=P(x)∨ P(f(a))∨ Q(x) C2= 172。 P(y)∨ R(b) 可見 ,在 C1 中有可合一的文字 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)) 2022/2/16 97 (5) 例 ： C＝ P(x) ?P(f(y)) ? 172。Q(x), σ={f(y)/x} Cσ ＝ P(f(y)) ? 172。Q(f(y))是 C的因子。 定義 13 子句 C中，兩個(gè)或兩個(gè)以上的文字有一個(gè)最 一般合一 σ ，則稱 Cσ 為 C的 因子 ，若 Cσ 為單元子句，則 Cσ 稱為 C的 單因子 。 2022/2/16 98 (6) 定義 14 子句的 C1， C2消解式，是下列二元消解式之一 : （ 1） C1和 C2的二元消解式； （ 2） C1和 C2的因子的二元消解式； （ 3） C1因子和 C2的二元消解式； （ 4） C1的因子和 C2的因子的二元消解式。 2022/2/16 99 謂詞邏輯中的歸結(jié)原理 (7) 定理 4 謂詞邏輯中的消解（歸結(jié)）式是它的親本子句 的邏輯結(jié)果。 謂詞邏輯的推理規(guī)則（ 消解原理 或 歸結(jié)原理 ）： C1 ? C2 ＝ （ C1 σ － {L1 σ}） ∪ （ C2 σ－ {L2 σ}） 其中 C C2是兩個(gè)無相同變?cè)淖泳洌?L1， L2分別是 C1， C2中的文字 ,σ 為 L1和 172。 L2的最一般合一。 2022/2/16 100 謂詞邏輯中的歸結(jié)原理 (8) 例 求證 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é)反演法，先證明 A1 ? A2 ?172。G是不可滿足的。 a. 求子句集： (1) 172。P(x) ?Q(x) (2) 172。P(y) ?R(y) (3) P(a) (4) S(a) (5) 172。S(z) ? 172。 R(z) (172。G) A2 A1 S 2022/2/16 101 謂詞邏輯中的歸結(jié)原理 (9) ，得： (6)R(a) [(2),(3), σ1={a/y}] (7) 172。 R(a) [(4),(5), σ2 ={a/z}] (8)Nil [(6),(7)] S是不可滿足的，從而 G是 A1和 A2的邏輯結(jié)果 。 a. 求子句集 S (1) 172。P(x) ?Q(x) (2) 172。P(y) ?R(y) (3) P(a) (4) S(a) (5) 172。S(z) ? 172。 R(z) 2022/2/16 102 求取謂詞邏輯的歸結(jié)式要注意 ? 謂詞的一致性 ：名稱不一致的謂詞 P與 172。Q不能歸結(jié) ? 常量的一致性 ：含有不同常量的謂詞不能歸結(jié)，如P(a,… )和 172。 P(b,… )不能歸結(jié)，但同樣謂詞，常量與變?cè)煌瑫r(shí)， P(a,… )和 172。 P(x,… )可以替換合一轉(zhuǎn)化成相同形式再歸結(jié) ? 變?cè)c函數(shù) ： P(x,x… )和 172。 P(f(x),f(x)… )不能歸結(jié) ,因?yàn)椴淮嬖谔鎿Q {f(x)/x}，但 P(x,x… )和 172。 P(f(y),f(y)… )可歸結(jié) ,因?yàn)榇嬖谔鎿Q {f(y)/x}， ? 不能同時(shí)消去兩個(gè)互補(bǔ)對(duì) ： P(x) ? Q(x)和 172。P(x) ? 172。 Q(x)不能直接得到□，因?yàn)檎嬷底C明 (P(x) ? Q(x))? (172。P(x) ? 172。 Q(x))不是矛盾式，推不出空子句。但P(x) ? P(y)和 172。P(u) ? 172。 P(v)可以合一替換歸結(jié)得到□， 2022/2/16 103 謂詞邏輯中的歸結(jié)原理 (10) 例 設(shè)已知： （ 1）能閱讀者是識(shí)字的； （ 2）海豚不識(shí)字； （ 3）有些海豚是很聰明的。 試證明：有些聰明者并不能閱讀。 證 首先定義如下謂詞： R(x):x能閱讀。 L(x):x能識(shí)字。 I(x):x是聰明的。 D(x):x是海豚。 將上述各語句翻譯成謂詞公式： (1) (?x)(R(x)?L(x)) (2) (?x)(D(x)?172。L(x)) 已知條件 (3) (?x)(D(x)?I(x)) (4) (?x)(I(x)?172。R(x)) 需證結(jié)論 2022/2/16 104 謂詞邏輯中的歸結(jié)原理 (11) 用歸結(jié)反演法來證明，求題設(shè)與結(jié)論否定的子句集，得： (1) 172。 R(x) ? L(x) (2) 172。 D(y) ? 172。L(y) （改名） (3) D(a) (4) I(a) (5) 172。 I(z) ? R(z) 歸結(jié)得： (6)R(a) [(5), (4),{a/z}] (7)L(a) [(6), (1),{a/x}] (8)172。D(a) [(7), (2),{a/y}] (9)Nil [(8), (3)] 172。 I(z) ? R(z) R(a) L(a) 172。 D(a) Nil I(a) 172。 R(x) ? L(x) 172。 D(y) ? L(y) D(a) 2022/2/16 105 謂詞邏輯中的歸結(jié)原理 (12) 定理 5 如果子句集 S是不可滿足的，那么必存在 一個(gè)由 S推出空子句的消解序列。 證明從略 2022/2/16 106 謂詞邏輯中的歸結(jié)原理 (13) 練習(xí) 設(shè)已知： （ 1）自然數(shù)都是大于零的整數(shù)； （ 2）所有整數(shù)不是偶數(shù)就是奇數(shù)； （ 3）偶數(shù)除以 2是整數(shù)。 試證明：所有自然數(shù)不是奇數(shù)就是除以 2為整數(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))) 2022/2/16 107 謂詞邏輯中的歸結(jié)原理 (14) 利用歸結(jié)反演法，先證明 F1 ? F2 ? F3 ? 172。G是不可滿足的。 F1 ? F2 ? F3 ? 172。G的子句集為 （ 1） 172。N(x) ? GZ(x) （ 2） 172。N(y) ? I(y) （ 4） 172。E(u) ? I(s(u)) （ 3） 172。I(z) ? E(z) ?O(z) （ 5） N(a) （ 6） 172。O(a) （ 7） 172。I(s(a)) 2022/2/16 108 應(yīng)用歸結(jié)原理進(jìn)行定理證明的方法思路 ? 寫出定理的謂詞公式 ? 用反演法表達(dá)謂詞公式 ? 化為 Skolem標(biāo)準(zhǔn)型 ? 求取子句集 S ? 對(duì) S中可歸結(jié)的子句做歸結(jié) ? 歸結(jié)式仍放在 S中，反復(fù)執(zhí)行歸結(jié)過程 ? 得到空子句 ? 得證。 2022/2/16 109 應(yīng)用歸結(jié)原理求取問題答案 (1) 例 已知： （ 1）如果 x和 y是同班同學(xué)，則 x的老師也是 y的老師。 （ 2）王先生是小李的老師。 （ 3）小李和小張是同班同學(xué)。 問：小張的老師是誰？ 解 首先定義如下謂詞： T(x,y)表示 x是 y的老師 C(x,y)表示 x與 y是同班同學(xué)。 已知條件可以表示成如下謂詞公式： F1： ?x ?y?z(C(x,y) ? T(z,x) ?T(z,y)) F2: T(Wang,Li) F3: C(Li,Zhang) 2022/2/16 110 應(yīng)用歸結(jié)原理求取問題答案 (2) 為了得到答案，首先要證明小張的老師是存在的。 即證明： G： ?xT(x,Zhang) (1) 172。C(x,y) ? 172。T(z,x) ? T(z,y) (2)T(Wang,Li) (3)C(Li,Zhang) (4) 172。T(u,Zhang) 求 F1 ? F2 ? F3? 172。 G的子句集： F1： ?x ?y?z(C(x,y