RGZN_5謂詞邏輯

1、第五章 基于謂詞邏輯的機器推理在許多應(yīng)用中，被編碼進入產(chǎn)生式系統(tǒng)數(shù)據(jù)庫的信息來源于說明語句，這些語句難以或者不能自然地用像數(shù)組或集合那樣的簡單結(jié)構(gòu)來表示。例如，機器人求解問題要求具有表達、檢索和變換語句集合的能力。而邏輯語句，或者更具體地說，一階謂詞演算能用來表示種類眾多的語句,且能給出一種從舊知識直接求得新知識的有效方法數(shù)學演繹。即如能證明一個新語句是從那些已知正確的語句導出的，那么我們就可斷定這個新語句也是正確的。證明的概念 推廣(把演繹包括在內(nèi))用來作為一種求取問題的方法。第一節(jié) 謂詞演算5.1.1 命題邏輯及其局限性 命題 具有真假意義的一句話人們研究用命題邏輯作為一種表達知識的方法，

2、因為它處理簡單，并存在一個判定方法。如:可把客觀世界的各種事實表示為邏輯命題，用命題邏輯把各種命題寫成合適公式（WFF）。例如：雨天 表示為: RAINING 晴天 表示為: SUNNY 霧天 表示為: FOGGY 若為雨天，則非晴天。 表示為： RAININGSUNNY但是，我們很快就會遇到命題邏輯的局限性。假定我們要表示由下列句子敘述的明顯事實： 李明是個工人可寫為 LIWORKER如果我們也要表示： 王華也是個工人就必須寫出 WANGWORKER這是一些完全獨立的格式，我們無法從中得出有關(guān)李（LI）和王（WANG）相似性的結(jié)論。 如果把這些事實表示為如下形式： WORKER（LI） WO

3、RKER（WANG）那么這就要好得多，因為這種表達結(jié)構(gòu)反映出知識本身的結(jié)構(gòu)。如果我們試圖用命題邏輯來表示下列句子： 所有的人都會死。那么我們將面臨更大的困難，因為如果我們不對問題進行量化，那么我們就必須一個一個地寫出某某某會命題邏輯局限性:l 不區(qū)分知識的結(jié)構(gòu)與成分;l 不可對問題進行量化而謂詞邏輯允許我們表達那些無法用命題邏輯相應(yīng)地加以表達的事情,可進行演繹,可使用變量及量詞( 、彐)。(x)(H(x) D(x)對任意x ,只要x是人 ,則x必然會死。5.1.2 謂詞邏輯的句法和語義 基本組成部分: 謂詞符號、變量符號、函數(shù)符號和常量符號，并用圓括弧、方括弧、花括弧和逗號隔開，以表示論域內(nèi)的

4、關(guān)系。 個體（客體）名稱集合（或稱論域）D 常量符號： 代表D中某一個確定個體 變量符號： 代表D中任一個個體（客體） 函數(shù)符號： f(x1,.,xn)它為Dn D 的一個映射（最終值D） 表達個體之間的對應(yīng)關(guān)系，例如：我們用father(x)表示x的父親。約定：小寫字母f,g,h等表示函數(shù)符號，小寫字母x,y,z,u,v,w等表示個體變量(變元)符號，小寫字母a,b,c等表示個體常量(常元)符號 謂詞符號： 由大寫字母（單詞）表示，定義域為Dn ，值域為T，F(xiàn) 的函數(shù)的函數(shù)名 項： 常量符號、變量符號、函數(shù)符號，（最終值D） 原子謂詞公式： P(t1,.,tm) 謂詞符號 項 如： P(x,

5、y,z) 命 題 ？ 變量 定義P關(guān)系：令P(x,y,z)表示x在y與z之間 命題 ？ 代入確定個體（實例化）：如令x,y,z代表北京、保定、石家莊， 則P(x,y,z)為命題。5.1.3 連詞和量詞合適公式（WFF）： 通過使用連詞（非）、（與）、（或）、=>（ 蘊涵，或隱含）以及 、彐等將原子謂詞公式按一定的語法格式連接而成的式子。連詞用來表示復合句子。例如，句子“我喜愛音樂和繪畫”可寫成： LIKE(I，MUSIC)LIKE(I，PAINTING)又如“李住在一幢黃色的房子里”，即可用 LIVES(LI，HOUSE-1)COLOR(HOUSE-1，YELLOW)其中謂詞LIVES表

6、示人與物體（房子）間的關(guān)系，而謂詞COLOR則表示物體與其顏色之間的關(guān)系。合?。?用連詞把幾個（原子）公式連接起來而構(gòu)成的公式此合取式的每個組成部分叫做合取項連詞用來表示可兼有的“或”。例如，句子“李明打藍球或踢足球”可表示為：PLAYS（LIMING，BASKETBALL）PLAYS（LIMING，F(xiàn)OOTBAL）析取： 用連詞把幾個公式連接起來所構(gòu)成的公式此析取式的每一組成部分叫做析取項 合取和析取的真值由其組成部分的真值決定。連詞 =>用來表示“如果-那么”的詞句。如句子“如果該書是何平的，那么它是藍色（封面）的”可表示為：OWNS(HEPING，BOOK-1) => COL

7、OR(BOOK-1，BLUE)又如，句子“如果劉華跑得最快，那么他取得冠軍”可表示為： RUNS(LIUHUA，F(xiàn)ASTEST) => WINS(LIUHUA，CHAMPION)用連詞=>連接兩個公式所構(gòu)成的公式叫做蘊涵。蘊涵的左式叫做前項，右式叫做后項。如果前項和后項都是合適公式，那么蘊涵也是合適公式。如果后項取值T（不管其前項的真值如何），或者前項取值F(不管后項的真值如何)，則蘊涵取值T；否則，蘊涵取值F。符號（非）用來否定一個公式的真值，也就是說，把一個合適公式的取值從T變?yōu)镕，或從F變?yōu)門。例如，子句“機器人不在2號房間內(nèi)”可表示為：INROOM（ROBOT，r2）前面具

8、有符號的公式叫做否定。 如果我們把句子限制為我們至今已介紹過的造句法所能表示的那些句子，而且也不使用變量項，那么我們可以把這個謂詞演算的子集叫做命題演算。命題演算對于許多簡化了的定義域來說，是一種有效的表示，但它缺乏用有效的方法來表達多個命題（如“所有的機器人都是灰色的”）的能力。要擴大命題演算的能力，我們需要使公式中的命題帶有變量。、彐 有時，一個原子公式如P（x），對于所有可能的變量x都具有值T。這個特性可由在P（x）前面加上全稱量詞（x）來表示。如果至少有一個x值可使P（x）具有值T，那么這一特性可由在P（x）前面加上存在量詞（彐x）來表示。例如，句子“所有的機器人都是灰色的”可表示為：

9、 （x）ROBOT（x）COLOR（x，GRAY）而句子“1號房間內(nèi)有個物體”可表示為: （彐x）INROOM（x，r1）x: 經(jīng)過量化了的約束變量： 如果一個合適公式中某個變量是經(jīng)過量化的，我們就把這個變量叫約束變量，否則就叫它為自由變量。句子： 在合適公式中，若所有變量都是受約束的。這樣的合適公式叫做句子。 值得指出的是，本書中所用到的謂詞演算為一階謂詞演算。不允許對謂詞符號或函數(shù)符號進行量化。例如，在一階謂詞演算中，（P）P（A）就不是合適公式。又例：每個有理數(shù)都是實數(shù)有些實數(shù)是有理數(shù)并非每個實數(shù)都是有理數(shù)解： 令 原子謂詞公式P(x) 表示 x 是有理數(shù) Q(x) 表示 x 是實數(shù)（x

10、）P(x) => Q(x)（彐x）Q(x) P(x) (（x）Q(x) => P(x) 等價于 （彐x）Q(x) P(x)例： 每一個人的外祖父都是他母親的父親。令 P(x) 表示 x 是人O(x,y) 表示 x 是y的外祖父F(x,y) 表示 x 是y的父親M(x,y) 表示 x 是y的母親將原句轉(zhuǎn)化為：每一個人y的外祖父x都是該y的母親z的父親。（x）（y）(P(x)P(y)O(x,y)=>(彐z)(P(z)F(x,z)M(z,y) 第二節(jié) 謂詞公式5.2.1 謂詞公式的定義原子謂詞公式 P(x1，x2，xn）合適公式：1.原子謂詞公式是合適公式。2.若A為合適公式，則A

11、也是一個合適公式。 5.若A和B都是合適公式，則（AB），（AB），（AB）和（A B）也都是合適公式。.若A是合適公式，x為任意變元，則（x）A和（彐x）A都是合適公式。.只有按上述規(guī)則1至4求得的那些公式，才是合適公式。5.2.2 合適公式的性質(zhì) 如果P和Q是兩個合適公式，則由這兩個合適公式所組成的復合表達式可由下列真值表給出。 P Q PQ PQ P =>Q P T T T T T F F T T F T T T F T F F F F F F F T T 如果兩個合適公式，無論如何解釋（取任何值），其真值表都是相同的，那么我們就稱此兩合適公式是等價的。 有如下等價關(guān)系：1. 否定

12、之否定（P） 等價于 P2. PQ 等價于 PQ5. 狄·摩根定律（PQ） 等價于 PQ（PQ） 等價于 PQ5.分配律P（QR） 等價于 （PQ）（PR）P（QR）等價于（PQ）（PR）5.交換律PQ 等價于 QPPQ 等價于 QP6.結(jié)合律（PQ）R 等價于 P（QR）（PQ）R 等價于 P（QR）7.逆否律PQ 等價于 QP此外，我們還可建立下列等價關(guān)系：8. （彐x）P(x) 等價于 （x）(P（x）)（x）P(x) 等價于 (彐x)(P（x）)9. （x）P（x）Q（x） 等價于（x）P（x）（x）Q（x）（彐x）P（x）Q（x）等價于（彐x）P（x）（彐x）Q（x）10.

13、 （x）P（x） 等價于 （y）P（y）（彐x）P（x） 等價于 （彐y）P（y）上述最后兩個等價關(guān)系說明，在一個量化的表達式中的約束變量是一個虛元，它可以用任何一個不在表達式中出現(xiàn)過的其他變量符號來代替。 下面用謂詞演算來表示英文句子：All blocks on top of blocks that have been moved or that are attached to block that have been moved also have been moved. 可表示為：（x）（y）BLOCK（x）BLOCK（y）ONTOP（x，y）ATTACHED（x，y）MOVED（y）M

14、OVED（x）5.2.3 推理規(guī)則、定理與證明假元推理 合適公式結(jié)論W2 W1W1W2 前提全稱消去推理（全稱化推理）它是由合適公式（x）W(x)產(chǎn)生合適公式W(A)，其中A為任意常量符號。同時應(yīng)用假元推理和全稱化推理，可由合適公式(x)W1(x)W2(x)結(jié)論W2(A)W1（A） 推理規(guī)則用來由已知的合適公式產(chǎn)生導出的合適公式。在謂詞邏輯中，這種導出的合適公式叫做定理，而所使用的推理規(guī)則的序列則構(gòu)成該定理的一個證明。在人工智能中，可以把某些問題求解任務(wù)當做某個定理求證的任務(wù)。在該證明中所應(yīng)用的推理序列給出了該問題的一個解答。5.2.4 永真性和可滿足性永真： 一個公式如果它們對所有可能的解釋

15、均取值T，則這個公式稱作為永真的，而永真的基公式一般叫做重言式。如：公式P（A）P（A）P（B）公式G的一個解釋I： 由非空域D以及對G中的常量符號、函數(shù)符號、謂詞符號的一組指定所構(gòu)成。公式G稱為可滿足的： 如果存在解釋I，使G在I下取T值。公式G稱為永真的： 如果G的所有解釋I，都使G取T值。如果每個滿足公式集S的解釋也滿足公式X，那么公式X邏輯上遵循公式集S。 凡使S中各公式為真者，必使公式X為真 X是S的邏輯結(jié)論例如： 結(jié) 論 X 前 提 S 公式 邏輯上遵循的公式集P（A） （x）P（x）（x）Q（x） （x）P（x）Q（x），（x）P（x）5.2.4 置換與合一 上一節(jié)講過，聯(lián)合使用

16、假元推理和全稱化推理，可以根據(jù)合適公式 （x）W1（x）W2（x） W1（A）產(chǎn)生 W2（A）這就需要尋找A對x的置換，使W1（A）與W1（x）一致。尋找項對變量的置換，以使表達式一致，叫做合一。合一是人工智能中很重要的過程。置換 ： 在一個表達式（謂詞公式）中用項（常量、變量、函數(shù)）去替換變量目的 ： 使多個表達式一致起來（以便進行歸結(jié)推理）例： 表達式Px，f（y），B的四個置換為： s1=z/x，w/y s2=A/y s3=g（z）/x，A/y s4=c/x，A/y 一般形式為： t1/V1,t2/V2, ,tn/Vn其中ti 為項，Vi 為互不相同變量，且Vi不出現(xiàn)于ti中，表示Vi同

17、時替換為ti 設(shè)表達式E經(jīng)置換S作用后，結(jié)果表達式為ES。則： Px，f（y），Bs1 = Pz，f（w），B Px，f（y），Bs2 = Px，f（A），B Px，f（y），Bs3 = Pg（z），f（A），B Px，f（y），Bs4 = Pc，f（A），B置換后的結(jié)果表達式ES為原表達式E的邏輯結(jié)論即ES在邏輯上遵循EES 也稱為E在 代換S下的一個例式 越置換，越具有特殊性 P(x) A/x P(A) 一般 特殊置換滿足結(jié)合律，但一般不滿足交換律。即用s1s2表示兩個置換s1與s2的合成，L表示一表達式，則有：（Ls1）s2 = L（s1s2）即用s1、s2相繼作用于L是同 s1s2作用

18、于L一致的以及 （s1s2）s3=s1（s2s3）但 s1s2s2s1定義： 設(shè)有表達式集Ei = E1 ，E2 ，En，若存在置換S，使E1S = E2 S = = EnS ，則稱S為集Ei的一個合一者（簡稱合一），也說表達式集是可合一的。例： P(a，y)，P(x，f(b)是可合一的 （因為存在置換 S =a/x,f(b)/y 是這個集的一個合一者）又例：Px，f（y），B，Px，f（B），B是可合一的，合一者為： S=A/x，B/y （實際上 A/x 多余的）另一合一者 g =B/y定義： 若g為Ei的一個合一者，對Ei的任一合一者S，都存在一個置換S，使得 EiS=Ei g S，則稱g

19、為Ei的最通用（最簡單的）合一者，記為mgu（Most General Unifier）。 如對上例，mgu為： g=B/y有許多算法可用來合一可合一表達式的有限集，并在該集不可合一時宣告失敗退出。求mgu的算法：非遞歸算法 定義： 設(shè)有一非空有限公式集F= F1 ，F(xiàn)2 ，F(xiàn)n，從F中各公式的第一個符號同時向右比較，直到發(fā)現(xiàn)第一個彼此不盡相同的符號止；從F的各個公式中取出那些從第一個不一致符號開始的最大子表達式，將這些子表達式作為元素組成一個集合D，稱為F的分歧集。如 F=Px，f(y，z)，Px，f(g(a),h(b) F的分歧集 D = y,g(a)合一算法：1、置 k=0; Fk =

20、F;k =; (其中Fk 為消除了k個分歧集后的公式集；F為原始公式集；k 為消除了前k個分歧集所用的置換； 空置換）2、若Fk 只含一個表達式，則算法停止，k 為所求最一般合一；3、找出Fk 分歧集Dk ；4、若Dk 中存在元素ak 和tk ,其中ak 為變量，tk為項，且ak 不在tk中出現(xiàn)，則置k+1=k· tk /ak ；Fk+1=Fk· tk /ak ； k = k +1; 轉(zhuǎn)步驟2；5、（第四步不滿足，算法停止，F(xiàn)的最一般合一者不存在）例：求公式集Pa，x，f(g(y)，Pz，h(z,u)，f(u)的最一般合一者 mgu。解： k=0; F0 = F; 0 =;

21、 F0 不是單一元素集，有 D0 =a ,z1=0· a /z =· a /z = a /z ；F1=F0· a /z =Pa，x，f(g(y)，Pa，h(a,u)，f(u)；k=1; F1 不是單一元素集，有 D1 =x ,h(a,u)2=1· h(a,u) /x = a /z · h(a,u) /x = a /z, h(a,u) /x ；F2=F1· h(a,u) /x =Pa，h(a,u)，f(g(y)，Pa，h(a,u)，f(u)； k=2; F2 非單一，有 D2 =g(y) ,u3=2· g(y) /u = a

22、/z, h(a,g(y) /x, g(y) /u ；F3=F2· g(y) /u =Pa，h(a, g(y)，f(g(y)； k=3;F3 已為單一元素集 3= a /z, h(a,g(y) /x, g(y) /u 為公式集F的mgu(2) 遞歸算法（類PASCAL描述的UNIFY遞歸過程）Procedure unify(E1，E2) E1，E2為本層次帶來欲合一的表達式 字符串型局部變量：F1 ,F2 ,T1 ,T2 ,Z1 ,Z2 , G1 ,G2 ; F1 ,F2 中存本次E1，E2的First元素 T1 ,T2 中存本次E1，E2的Tail部分 Z1 中存F1 ,F2 的合一

23、者，Z2中存T1 ,T2的合一者 首元素F1 ,F2 的合一者Z1 作用于剩余部分T1 ,T2后的結(jié)果放G1 ,G2 BEGINif E1或E2中有一個是原子（即謂詞符號、函數(shù)符號、常量符號、否定符號或變量）then 遞歸出口 beginif E1和E2是相同的，thenreturn NIL;不用置換，就已相同 if E1非原子 then 交換E1和E2的位置,使E1是原子; if E1是變量,且E1不出現(xiàn)在E2中 then returnE2/E1 ; if E2是變量then returnE1/E2 else return FAIL; end else E1,E2均非原子時begin F1:

24、=E1的第一個元素;T1:=E1的其余元素;F2:=E2的第一個元素;T2:=E2的其余元素; Z1:=unify(F1,F2);將首元素合一，合一式在Z1中 if Z1=FAIL then return FAIL; 首元素不可合一， 則整體不可合一 G1：=Z1作用到T1的結(jié)果； G2：=Z1作用到T2的結(jié)果； Z2：=unify(G1，G2）；將剩余部分當作新表達式去合一，遞歸調(diào)用 if Z2=FAIL then return FAIL；return Z1與Z2的合成Z1·Z2endEND.遞歸具體實現(xiàn)方案將各種單括號及逗號視為元素及原子加入遞歸之中原子：（1）謂詞符號、常量符號

25、、變量符號、函數(shù)符號、否定符號 (2)各種單括號： 圓、方、花括弧(3)逗號E1、E2的第一個元素為：謂詞符號、常量符號、變量符號、函數(shù)符號(參數(shù)部分)、否定符號、單括號、逗號若F1與F2均為函數(shù)時，則令F1、F2均取函數(shù)符號部分，而將括號中的參數(shù)部分劃歸至T1、T2，再去遞歸處理。（否則的話，連同參數(shù)部分一起拿出當作第一元素）例：E1=Pa，x，f(g(y)E2=Pz，h(z,u)，f(u)則： unify(E1,E2); Z1:=unify(P,P)Z2:= unify(a ,.,z,) return Z1·Z2取值分析第i層次 F1值 F2值 Z1值 F1屬性 F2屬性 1 P

26、 P 謂詞符號 謂詞符號 2 方括號 方括號 3 a z a/z 常量符號 變量符號 4 ， ， 5 x h(a,u) h(a,u)/x 變量 函數(shù)符號(參數(shù)) 6 , , 逗號 逗號 7 f f 函數(shù)符號 函數(shù)符號 8 ( ( 圓括號 圓括號 9 g(y) u g(y)/u 函數(shù)符號(參數(shù)) 變量 10 ) ) 圓括號 圓括號 11 方括號 方括號 第三節(jié) 歸結(jié)原理定義 歸結(jié): 是一種可用于一定的子句公式的重要推理規(guī)則。子句: 定義為由文字的析取組成的公式文字: 一個原子公式和原子公式的否定結(jié)論： 任意謂詞公式都可化為子句集5.5.1 將謂詞公式化為子句集的步驟1. 消去蘊涵符號 =>

27、只應(yīng)用和符號， AB 替換 AB2. 的深入 （反復應(yīng)用狄·摩根定律）AB 代替 （AB）AB 代替 （AB）A 代替 （A）（x）A 代替 （彐x）A（彐x）A 代替 （x）A5. 量詞變元唯一（變量標準化）在任一量詞轄域內(nèi)，受該量詞約束的變量為一啞元（虛構(gòu)變量），它可以在該轄域內(nèi)處處統(tǒng)一地被另一個沒有出現(xiàn)過的任意變量所代替，而不改變公式的真值。合適公式中變量的標準化意味著對啞元改名以保證每個量詞有其自己唯一的啞元。例如，（x）P（x）（彐x）Q（x）標準化而得到： （x）P（x）（彐y）Q（y）4. 消去 彐存在量詞是在全稱量詞的轄域內(nèi)，我們允許所存在的x可能依賴于y值。令這種依

28、賴關(guān)系明顯地由函數(shù)g（y）所定義，它把每個y值映射到存在的那個x。這種函數(shù)叫做Skolem函數(shù)。如果用Skolem函數(shù)代替存在的x，我們就可以消去全部存在量詞,但函數(shù)符號不能同于公式中已有函數(shù)。 如： （x）（y）（彐z） P（x，y,z） 消去 彐, 寫成 （x）（y）P（x，y,f(x,y)） ii) 如果要消去的存在量詞不在任何一個全稱量詞的轄域內(nèi)，那么我們就用不含變量的Skolem函數(shù)即常量代換。 例如，（彐x）P（x）化為P（A） 其中常量符號A用來表示我們知道的存在實體。A必須是個新常量符號，它未曾在公式中其他地方使用過。5. 化為前束形到這一步，已不留下任何存在量詞，而且每個全稱

29、量詞都有自己的變量。把所有全稱量詞移到公式的左邊，并使每個量詞的轄域包含這個量詞后面公式的整個部分。所得公式稱為前束形。前束形公式由前綴和母式組成，前綴由全稱量詞串組成，母式由沒有量詞的公式組成，即： 前束形 =（前綴） 母 式 全稱量詞串 無量詞公式6. 把母式化為合取范式 任何母式都可寫為由一些謂詞公式和（或）謂詞公式的否定的析取的有限集組成的合取。這種母式叫做合取范式。我們可以反復應(yīng)用分配律，把任一母式化成合取范式。例如， 把ABC化為： ABAC7. 消去全稱量詞 到了這一步，所有余下的量詞均被全稱量詞量化了。同時，全稱量詞的次序也不重要了。因此，我們可以消去前綴，即消去明顯出現(xiàn)的全稱

30、量詞。8. 消去連詞符號用A，B代替（AB），以消去明顯的符號。反復代替的結(jié)果，最后得到一個有限集，其中每個公式是文字的析取。9. 更換變量名稱 可以更換變量符號的名稱，使一個變量符號不出現(xiàn)在一個以上的子句中。例 將下列謂詞公式 （x）P（x）（y）P(y)P(f(x,y)（y）Q(x,y)P（y）按標準步驟化為子句集。解： (1) (x)P(x)(y)P(y)P(f(x,y) (y)Q（x，y）P（y）(2) (x)P（x）(y)P(y)P(f(x,y) （彐y）Q（x，y）P（y）(x)P（x）(y)P(y)P(f(x,y) （彐y）Q（x，y）P（y）(3) (x)P（x）(y)P(y)

31、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） 式中，g（x）為一Skolem函數(shù)。(5) (x)(y)P（x）P(y)P(f(x,y)Q（x，g（x）P（g（x）(6) (x)(y)P（x）P（y）P（f（x，y）P（x）Q（x，g（x）P（x）P（g（x）(7) P（x）P（y）P（f（x，y）P（x）Q（x，g（x）P（x）P（g（x）(8) P（x）P（y）P（f（x，y） P（x）Q（x，g（x） P（x）P（g（x）(9)更改變量名稱，在上述第(8)步的三個子句中，我們分別以x1，x2和x3代替變量x。

32、這種更改變量名稱的過程，有時稱為變量分離標準化。于是，我們可以得到下列子句集：P（x1）P（y）Pf（x1，y）P（x2）Qx2，g（x2）P（x3）Pg（x3）必須指出，一個子句內(nèi)的文字可含有變量，但這些變量總是被理解為全稱量詞量化了的變量。如果一個表達式中的變量被不含變量的項所置換，則我們得到稱為文字基例的結(jié)果。例如，QA，f（g（B）就是Q（x，y）的一個基例。在定理證明系統(tǒng)中，歸結(jié)作為推理規(guī)則使用時，我們希望從公式集來證明某個定理，首先就要把公式集化為子句集。可以證明，如果公式X在邏輯上遵循公式集S，那么X在邏輯上也遵循由S的公式變換成的子句集。即當希望證明: “若公式集S成立,則可推

33、出X成立?！笨勺?yōu)樽C明：若公式集S變換成的子句集成立,則可推出X成立。5.5.2 歸結(jié)推理規(guī)則令L1為任一原子公式，L2為另一原子公式；L1和L2具有相同的謂詞符號，但一般具有不同的變量；L2為L2的否定。結(jié)論： 若兩子句具有形式L1和L2，且L1和L2具有最一般合一者時，則任一使L1及L2為真的解釋必使()·為真。即是說()·必為兩前提子句L1及L2的邏輯結(jié)論 ；或說可從兩父輩子句推導出新子句，叫歸結(jié)式。它是由取這兩個子句的析取，然后消去互補對而得到的。推論： 兩前提子句具有形式L112i及L112j則可導出結(jié)論子句 12i12j例： 前提1 前提2 結(jié)論（歸結(jié)式）PR

34、PQ RQPQR QS PRSP PQ QPQ PQ QQ = QPQ PQ QQ Q=>Q 重言式PP P=>PP P ？PQ QR PR 鏈環(huán)式(三段論)5.5.3 含有變量子句的歸結(jié)讓我們把上述簡單的對基子句的歸結(jié)推理規(guī)則推廣到含有變量的子句。情況1： （有明顯互補）P(X) Q(X) P（X）R(f(A) 歸結(jié)式 Q(X)R(f(A)情況2： （靠合一產(chǎn)生互補）P(x,f(y) Q(x) R(f(a),y)R(z,w) P（f(f(a),z）令 = f(f(a)/x, f(y)/z 有歸結(jié)式：Q(f(f(a) R(f(a),y) R(f(y),w) 歸結(jié)兩個子句時，可能有一

35、個以上的歸結(jié)式，但任何情況下，最多只有有限個歸結(jié)式。 一般歸結(jié)規(guī)則：設(shè)有兩個子句 Li與Mi，若 li 是Li的一個子集，mi是Mi的一個子集，且存在一個最一般合一者s, 使得 lis=mis ,則可歸結(jié)前提子句Li與Mi成為Li-lisMi-mis例：我們考慮兩個子句：Px，f（A）Px，f（y）Q（y）和 Pz，f（A）Q（z） 如果我們?nèi)?li = Px，f（A） mi = Pz，f（A）那么我們得到歸結(jié)式：Pz，f（y）Q（z）Q（y）如果我們?nèi)?li = Q（y） mi = Q（z）那么我們得到歸結(jié)式： Px，f（A）Px，f（y）Py，f（A）進一步歸結(jié)得歸結(jié)式： Py，f（y）可

36、見對這兩個子句歸結(jié)一共可得四個不同的歸結(jié)式，其中三個是歸結(jié)P得到的，而另一個是由歸結(jié)Q得到的。第四節(jié) 謂詞演算在定理證明中的應(yīng)用 在典型的定理證明系統(tǒng)中，歸結(jié)通過反演產(chǎn)生證明。也就是說，要證明某個命題，其目標公式被否定并化成子句形，然后添加到命題公式集中去，把歸結(jié)反演系統(tǒng)應(yīng)用于聯(lián)合集，并推導出一個空子句（NIL），表示產(chǎn)生一個矛盾，從而使定理得到證明。這種歸結(jié)反演的證明思想，與數(shù)學中反證法的思想十分相似。 5.4.1 歸結(jié)反演設(shè)有前提公式集S，欲證結(jié)論公式L。步驟如下： (1)否定L，得L； (2)把L添加到S中去； (3)把新產(chǎn)生的集合L，S化成子句集； (4)應(yīng)用歸結(jié)原理，力圖推導出一個表

37、示矛盾的空子句。歸結(jié)反演的正確性。公式L在邏輯上遵循公式集S 任一使S為真的解釋必使L為真，即是說：不存在這樣的解釋，它使S與L同時為真，也即SL是不可滿足的。 SL是不可滿足的能從S，L子句集通過多次歸結(jié)操作產(chǎn)生一個空子句NIL例：前提： 每個儲蓄錢的人都獲得利息。 結(jié)論： 如果沒有利息，那么就沒有人去儲蓄錢。 證明： 令S（x，y）表示“x儲蓄y”M（x）表示“x是錢”I（x）表示“x是利息”E（x，y）表示“x獲得y”于是我們可把上述命題寫成下列形式：前提： ( x)（彐y）(S(x,y)M(y)（彐y）(I(y)E(x,y)結(jié)論：（彐x）I(x)(x) (y)(S(x,y)M(y) 把

38、前提化為子句形： ( x) （彐y）(S(x,y)M(y)（彐y）(I(y)E(x,y) ( x)( y) (S(x,y) M(y)（彐y）(I(y)E(x,y) 令y=f(x)為Skolem函數(shù),則可得子句形如下： (1)S（x，y）M（y）I(f(x) (2)S（x，y）M（y）E(x，f(x) 又結(jié)論的否定為： (彐x)I(x)(x)( y)(S(x,y)M(y) 化為子句形： (彐x)I(x)(x)( y)(S(x,y)M(y) (彐x)I(x)(x)( y)(S(x,y)M(y)(x)(I(x)(彐x)(彐y)(S(x,y)M(y)變量分離標準化之后得下列各子句：(3)I（z） (4

39、)S（a，b） (5)M（b）子句(1) 子句(3) f(x)/zS(x,y)M(y)子句(6) 子句(4) a/x,b/yNILM(b) 子句(7) 子句(5) 儲蓄問題反演樹例: 對于所有的x和y，如果x是y的父親，y是z的父親，那么x是z的祖父。每個人都有一個父親。是否會有這樣的兩個人x和y，使得x是y的祖父？證明： 令 F(x,y)表示“x是y的父親” G(x,y)表示“x是y的祖父”把命題寫成下列公式： (1) (x) (y) (z) (F(x,y)F(y,z)G(x,z) (2) (y)(彐x) F(x,y) (3) (彐x)(彐y)G(x,y)其中，公式(3)是我們試圖證明的結(jié)論

40、。 將公式(1)、(2)化為子句形，得：（1）F（x，y）F（y，z）G（x，z）（2）F（f（w），w）x=f（w）為一Skolem函數(shù)取公式(3)的否定： (3) (彐x)(彐y)G(x,y) 得其子句形為： （3）G（u，v）子句(1) 子句(3) u/x,v/zF(u ,y)F(y ,v) 子句(2) f(w)/y,v/wF(u , f(v) 子句(2) f(w)/u,f(v)/w NIL 祖孫問題反演樹 歸結(jié)反演系統(tǒng)的基本算法： 設(shè)已把各前提式與結(jié)論式的否定化成了所要求的子句集形式,并放在集合S中(1) CLAUSES S(2) WHILE NIL不為CLAUSES 的成員 do(3

41、) begin(4) 在CLAUSES中選取兩個不同的可歸結(jié)子句ci和cj(5) 計算ci和cj的歸結(jié)式rij(6) 把rij附加到子句集中，產(chǎn)生新的子句集(7) end如: (1)PQ (2) PQ (3)PQ (4) PQ可歸結(jié)的子句對有:直接應(yīng)用歸結(jié)原理，將對應(yīng)于一個反演的簡單的寬度優(yōu)先搜索。寬度優(yōu)先搜索方法:第i級歸結(jié)式是這樣的歸結(jié)式,其最近的父輩子句之一是第i-1級的歸結(jié)式,而另一父輩子句則為第0至第i-1級之中的任一子句。具體做法是： 首先將S0（第0級即初始子句集）的子句排序。之后，順序考慮S0 與S0之間的歸結(jié)式，得第一級歸結(jié)式集合S1=C12|C1S0，C2S0，然后檢查NI

42、L是否S1，是則結(jié)束，否則繼續(xù)考慮S0S1與S1之間的歸結(jié)式，得第二級歸結(jié)式集合S2=C12|C1S0S1，C2S1，然后檢查NIL是否S2，如： (1) PQS0: (2) PQ (3) PQ (4) PQ (5) Q 1-2 (6) P 1-3 (7) QQ 1-4(i) S1: (8) PP 1-4(ii) (9) QQ 2-3(i) (10) PP 2-3(ii) (11) P 2-4 (12) Q 3-4 S2: ? NIL ?例： 前提 （1）(x) R(x)=>L(x) 任何能閱讀的人都是能識字的。（2）(x) D(x)=> L(x) 任何海豚都不識字。（3）(彐x)

43、 D(x) I(x) 有些海豚是有智力的。 結(jié)論：（4）(彐x) I(x) R(x) 有些有智力者不能閱讀。 解： 將(1)(2)(3)及(4)的否定化成子句集： (1) I(A)S0: (2) I(z)R(z) (3) R(x) L(x)(4) D(y)L(y) (5) D(A) (6)R(A) 1-2 A/zS1: (7) I(z)L(z) 2-3 z/x(8) R(y) D(y) 3-4 y/x (9) L(A) 4-5 A/y (10) L(A) 1-7 A/z (11) I(z) D(z) 2-8 z/y (12) L(A) 3-6 A/x S2: (13) R(A) 3-9 A/x

44、 (14) I(z) D(z) 4-7 z/y (15) R(A) 5-8 A/y (16) D(A) 6-8 A/y (17) I(A) 7-9 A/z S3 ? NIL ?歸結(jié)搜索策略基本上可分為三種類型：簡化策略、改進策略和排序策略。5.4.2 簡化策略若某子句集是不可滿足的經(jīng)過若干次下述三種消去后的該子句集是不可滿足的1.重言式消去法 若某子句中含有一個文字及其否定的話，則可消去該子句。例如，子句 P（x）B（y）B（y）和 P（f（A）P（f（A）均可消去。2.謂詞估算消去法若某子句中某一文字估算為T，則可消去該文字所在的那一個子句。 若某子句中某一文字估算為F，則可消去該文字。例如，設(shè)E(x,y)表示x=y，那么子句P（x）Q（