基于謂詞邏輯的機(jī)器推理課件

1、第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 第 5 章 基于謂詞邏輯的機(jī)器推理 5.1 一階謂詞邏輯一階謂詞邏輯5.2 5.2 歸結(jié)演繹推理歸結(jié)演繹推理 5.3 5.3 應(yīng)用歸結(jié)原理求取問題答案應(yīng)用歸結(jié)原理求取問題答案 5.4 5.4 歸結(jié)策略歸結(jié)策略 5.5 5.5 歸結(jié)反演程序舉例歸結(jié)反演程序舉例 5.6 Horn5.6 Horn子句歸結(jié)與邏輯程序子句歸結(jié)與邏輯程序 5.7 5.7 非歸結(jié)演繹推理非歸結(jié)演繹推理 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.1 一階謂詞邏輯一階謂詞邏輯 5.1.1 5.1.1 謂詞、函數(shù)、量詞謂詞、函數(shù)、量詞 設(shè)a1,

2、 a2, , an表示個(gè)體對(duì)象, A表示它們的屬性、狀態(tài)或關(guān)系, 則表達(dá)式 A(a1, a2, , an) 在謂詞邏輯中就表示一個(gè)(原子)命題。 例如, (1) 素?cái)?shù)(2), 就表示命題“2是個(gè)素?cái)?shù)”。 (2) 好朋友(張三, 李四), 就表示命題“張三和李四是好朋友”。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 P(x1,x2,xn)一般地, 表達(dá)式 在謂詞邏輯中稱為n元謂詞。其中P是謂詞符號(hào)，也稱謂詞，代表一個(gè)確定的特征或關(guān)系(名)。x1,x2,xn稱為謂詞的參量或者項(xiàng)，一般表示個(gè)體。 個(gè)體變?cè)淖兓秶Q為個(gè)體域（或論述域），包攬一切事物的集合稱為全總個(gè)體域。第第5

3、5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 為了表達(dá)個(gè)體之間的對(duì)應(yīng)關(guān)系，我們引入通常數(shù)學(xué)中函數(shù)的概念和記法。例如我們用father(x)表示x的父親，用sum(x,y)表示數(shù)x和y之和，一般地，我們用如下形式：f(x1,x2,xn)表示個(gè)體變?cè)獂1,x2,xn所對(duì)應(yīng)的個(gè)體y，并稱之為n元個(gè)體函數(shù)，簡(jiǎn)稱函數(shù)（或函詞、函詞命名式）。其中f是函數(shù)符號(hào)，有了函數(shù)的概念和記法，謂詞的表達(dá)能力就更強(qiáng)了。例如，我們用Doctor(father(Li)表示“小李的父親是醫(yī)生”，用E(sq(x),y)表示“x的平方等于y”。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 以后我們約定用大

4、寫英文字母作為謂詞符號(hào),用小寫字母f,g, h等表示函數(shù)符號(hào),用小寫字母x, y, z等作為個(gè)體變?cè)?hào), 用小寫字母a, b, c等作為個(gè)體常元符號(hào)。 我們把“所有”、“一切”、“任一”、“全體”、“凡是”等詞統(tǒng)稱為全稱量詞, 記為 x; 把“存在”、“有些”、“至少有一個(gè)”、 “有的”等詞統(tǒng)稱為存在量詞, 記為x。 )()(xNxMx其中M(x)表示“x是人”, N(x)表示“x有名字”, 該式可讀作“對(duì)于任意的x, 如果x是人, 則x有名字”。這里的個(gè)體域取為全總個(gè)體域。如果把個(gè)體域取為人類集合, 則該命題就可以表示為)(xxN第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理

5、 同理, 我們可以把命題“存在不是偶數(shù)的整數(shù)”表示為 )()(xExGx其中G(x)表示“x是整數(shù)”, E(x)表示“x是偶數(shù)”。此式可讀作“存在x, x是整數(shù)并且x不是偶數(shù)”。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 不同的個(gè)體變?cè)? 可能有不同的個(gè)體域。為了方便和統(tǒng)一起見, 我們用謂詞表示命題時(shí),一般總?cè)∪倐€(gè)體域, 然后再采取使用限定謂詞的辦法來指出每個(gè)個(gè)體變?cè)膫€(gè)體域。 具體來講,有下面兩條： (1) 對(duì)全稱量詞,把限定謂詞作為蘊(yùn)含式之前件加入, 即 x(P(x)。 (2) 對(duì)存在量詞, 把限定量詞作為一個(gè)合取項(xiàng)加入, 即 x(P(x)。 這里的P(x)就是限定謂

6、詞。 我們?cè)倥e幾個(gè)例子。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例 5.1不存在最大的整數(shù), 我們可以把它翻譯為 ),()()(yxDyGyxGx或 ),()()(xyDyGyxGx例例 5.2對(duì)于所有的自然數(shù), 均有x+yx ),()()(xyxSyNxNyx例例 5.3某些人對(duì)某些食物過敏 ),()()(yxGyFxMyx第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.1.2 謂詞公式謂詞公式定義定義1 (1) 個(gè)體常元和個(gè)體變?cè)际琼?xiàng)。 (2) 設(shè)f是n元函數(shù)符號(hào),若t1,t2,tn是項(xiàng),則f(t1,t2,tn)是項(xiàng)。 (3) 只有有限次使用(

7、1), (2)得到的符號(hào)串才是項(xiàng)。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義2 設(shè)P為n元謂詞符號(hào)，t1,t2,tn為項(xiàng)，則P(t1,t2,tn)稱為原子謂詞公式，簡(jiǎn)稱原子公式或者原子。 從原子謂詞公式出發(fā)，通過命題聯(lián)結(jié)詞和量詞，可以組成復(fù)合謂詞公式。下面我們給出謂詞公式的嚴(yán)格定義，即謂詞公式的生成規(guī)則。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義3 (1)原子公式是謂詞公式。 (2)若A,B是謂詞公式，則A,AB,AB,AB, A B, xA, xA也是謂詞公式。 (3)只有有限步應(yīng)用(1)，(2)生成的公式才是謂詞公式。 由項(xiàng)的定義，

8、當(dāng)t1,t2,tn全為個(gè)體常元時(shí)，所得的原子謂詞公式就是原子命題公式（命題符號(hào)）。所以，全體命題公式也都是謂詞公式。謂詞公式亦稱為謂詞邏輯中的合適（式）合適（式）公式公式，記為Wff。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 緊接于量詞之后被量詞作用(即說明)的謂詞公式稱為該量詞的轄域。例如： (1) xP(x)。 (2) x(H(x)G(x, y)。 (3) xA(x)B(x)。其中(1)中的P(x)為x的轄域, (2)中的H(x)G(x, y)為x的轄域, (3)中的A(x)為x的轄域, 但B(x)并非x的轄域。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器

9、推理 量詞后的變?cè)?x, y中的x,y稱為量詞的指導(dǎo)變?cè)?或作用變?cè)?, 而在一個(gè)量詞的轄域中與該量詞的指導(dǎo)變?cè)嗤淖冊(cè)Q為約束變?cè)? 其他變?cè)?如果有的話)稱為自由變?cè)? 例如(2)中的x為約束變?cè)? 而y為自由變?cè)? (3)中A(x)中的x為約束變?cè)? 但B(x)中的x為自由變?cè)?。例?3),一個(gè)變?cè)谝粋€(gè)公式中既可約束出現(xiàn), 又可自由出現(xiàn), 但為了避免混淆, 通常通過改名規(guī)則, 使得一個(gè)公式中一個(gè)變?cè)獌H以一種形式出現(xiàn)。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 約束變?cè)母拿?guī)則如下： (1) 對(duì)需改名的變?cè)? 應(yīng)同時(shí)更改該變?cè)诹吭~及其轄域中的所有出現(xiàn)。 (2)

10、 新變?cè)?hào)必須是量詞轄域內(nèi)原先沒有的, 最好是公式中也未出現(xiàn)過的。例如公式 xP(x)Q(x)可改為 yP(y)Q(x), 但兩者的意義相同。 在謂詞前加上量詞, 稱作謂詞中相應(yīng)的個(gè)體變?cè)涣炕? 例如xA(x)中的x被量化, yB(y)中y被量化。如果一個(gè)謂詞中的所有個(gè)體變?cè)急涣炕? 則這個(gè)謂詞就變?yōu)橐粋€(gè)命題。例如, 設(shè)P(x)表示“x是素?cái)?shù)”,則 xP(x), xP(x)就都是命題。這樣我們就有兩種從謂詞(即命題函數(shù))得到命題的方法：一種是給謂詞中的個(gè)體變?cè)雮€(gè)體常元, 另一種就是把謂詞中的個(gè)體變?cè)苛炕?第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 把上面關(guān)于量

11、化的概念也可以推廣到謂詞公式。于是，我們便可以說，如果一個(gè)公式中的所有個(gè)體變?cè)急涣炕?，或者所有變?cè)际羌s束變?cè)ɑ驘o自由變?cè)?，則這個(gè)公式就是一個(gè)命題。特別地，我們稱 xA(x)為全稱命題， xA(x)為特稱命題。對(duì)于這兩種命題，當(dāng)個(gè)體域?yàn)橛邢藜瘯r(shí)（設(shè)有n個(gè)元素），有下面的等價(jià)式： xA(x)A(a1)A(a2)A(an) xA(x)A(a1)A(a2)A(an) 這兩個(gè)式子也可以推廣到個(gè)體域?yàn)榭蓴?shù)無限集。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義4 設(shè)A為如下形式的謂詞公式：B1B2Bn 其中Bi(i=1,2,n)形如L1L2Lm，Lj(j=1,2,m)為原子公

12、式或其否定，則A稱為合取范式。 例如： (P(x)Q(y)(乛P(x)Q(y)R(x,y)(乛Q(y)乛R(x,y) 就是一個(gè)合取范式。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義5 設(shè)A為如下形式的命題公式： B1B2Bn 其中Bi(i=1,2,n)形如L1L2Lm，Lj(j=1,2,m)為原子公式或其否定，則A稱為析取范式。 例如： (P(x)乛Q(y)R(x,y)(乛P(x) Q(y)(乛P(x)R(x,y) 就是一個(gè)析取范式。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義6 設(shè)P為謂詞公式，D為其個(gè)體域，對(duì)于D中的任一解釋I： (1)若

13、P恒為真，則稱P在D上永真（或有效）或是D上的永真式。 (2)若P恒為假，則稱P在D上永假（或不可滿足）或是D上的永假式。 (3)若至少有一個(gè)解釋,可使P為真，則稱P在D上可滿足或是D上的可滿足式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義7 設(shè)P為謂詞公式，對(duì)于任何個(gè)體域：(1)若P都永真，則稱P為永真式。(2)若P都永假，則稱P為永假式。(3)若P都可滿足，則稱P為可滿足式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.1.3 謂詞邏輯中的形式演繹推理謂詞邏輯中的形式演繹推理 由上節(jié)所述，我們看到，利用謂詞公式可以將自然語言中的陳述語句表

14、示為一種形式化的符號(hào)表達(dá)式。那么，利用謂詞公式，我們同樣可以將形式邏輯中抽象出來的推理規(guī)則形式化為一些符號(hào)變換公式。表3.1和表3.2就是形式邏輯中常用的一些邏輯等價(jià)式和邏輯蘊(yùn)含式，即推理規(guī)則的符號(hào)表示形式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 表表5.1 常用邏輯等價(jià)式常用邏輯等價(jià)式 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 表5.2 常用邏輯蘊(yùn)含式 第第5 5章

15、章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.4 設(shè)有前提： (1)凡是大學(xué)生都學(xué)過計(jì)算機(jī)； (2)小王是大學(xué)生。 試問：小王學(xué)過計(jì)算機(jī)嗎？ 解 令S(x)：x是大學(xué)生;M(x)：x學(xué)過計(jì)算機(jī); a：小王。則上面的兩個(gè)命題可用謂詞公式表示為 (1) x(S(x)M(x) (2) S(a) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 下面我們進(jìn)行形式推理： (2) x(S(x)M(x) 前提 (2)S(a)M(a) (1),US (3)S(a) 前提 (4)M(a) (2),(3),I3 得結(jié)果：M(a)

16、，即“小王學(xué)過計(jì)算機(jī)”。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.5 證明乛P(a,b)是 x y(P(x,y)W(x,y)和乛W(a,b)的邏輯結(jié)果。證 (1) x y(P(x,y)W(x,y) 前提 (2) y(P(a,y)W(a,y) (1),US (3) P(a,b)W(a,b) (2),US (4)乛W(a,b) 前提 (5)乛P(a,b) (3),(4),I4第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例5.6 證 x(P(x)Q(x) x(R(x)乛Q(x) x(R(x)乛P(x)。證證(1) x(P(x)Q(x) 前提(2)P(y

17、)Q(y) (1),US(3)乛Q(y)乛P(y) (2),E24(4) x(R(x)Q(x) 前提(5)R(y)乛Q(y) (3),US(6)R(y)乛P(y) (3),(5),I6(7) x(R(x)乛P(x) (6),UG 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.2.1 子句集子句集 定義定義1 原子謂詞公式及其否定稱為文字，若干個(gè)文字的一個(gè)析取式稱為一個(gè)子句，由r個(gè)文字組成的子句叫r文字子句，1文字子句叫單元子句，不含任何文字的子句稱為空子句，記為或NIL。 例如下面的析取式都是子句 PQ乛R P(x,y)乛Q(x)5.2 歸結(jié)演繹推理歸結(jié)演繹推理第第5 5章

18、章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義2 對(duì)一個(gè)謂詞公式G，通過以下步驟所得的子句集合S，稱為G的子句集。 (1)消去蘊(yùn)含詞和等值詞?？墒褂眠壿嫷葍r(jià)式: ABAB A B(乛AB)(乛BA)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (2)縮小否定詞的作用范圍，直到其僅作用于原子公式。可使用邏輯等價(jià)式: 乛(乛A) A 乛(AB) 乛A乛B 乛(AB) 乛A乛B乛 xP(x) x乛P(x)乛 xP(x) x乛P(x)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (3)適當(dāng)改名，使量詞間不含同名指導(dǎo)變?cè)图s束變?cè)?(4)消去存在量詞。 消去

19、存在量詞時(shí)，同時(shí)還要進(jìn)行變?cè)鎿Q。變?cè)鎿Q分兩種情況： 若該存在量詞在某些全稱量詞的轄域內(nèi)，則用這些全稱量詞指導(dǎo)變?cè)囊粋€(gè)函數(shù)代替該存在量詞轄域中的相應(yīng)約束變?cè)?，這樣的函數(shù)稱為Skolem函數(shù)； 若該存在量詞不在任何全稱量詞的轄域內(nèi)，則用一個(gè)常量符號(hào)代替該存在量詞轄域中的相應(yīng)約束變?cè)?，這樣的常量符號(hào)稱為Skolem常量。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (5)消去所有全稱量詞。 (6)化公式為合取范式。 可使用邏輯等價(jià)式: A(BC) (AB)(AC) (AB)C (AC)(BC) (7)適當(dāng)改名，使子句間無同名變?cè)?(8)消去合取詞，以子句為元素組成一個(gè)集合S。

20、第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.7 求下面謂詞公式的子句集 x yP(x,y) yQ(x,y)R(x,y)解解由步(1)得 x乛yP(x,y)乛 yQ(x,y)R(x,y)由步(2)得 x yP(x,y) yQ(x,y)乛R(x,y)由步(3)得 x yP(x,y) zQ(x,z)乛R(x,z)由步(4)得 x乛P(x,f(x)Q(x,g(x)乛R(x,g(x)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 由步(5)得乛P(x,f(x)Q(x,g(x)乛R(x,g(x)由步(6)得乛P(x,f(x)Q(x,g(x)乛P(x,f(x)乛R(x

21、,g(x)由步(7)得乛P(x,f(x)Q(x,g(x)乛P(y,f(y)乛R(y,g(y)由步(8)得乛P(x,f(x)Q(x,g(x),乛P(y,f(y)乛R(y,g(y)或乛P(x,f(x)Q(x,g(x)乛P(y,f(y)R(y,g(y) 為原謂詞公式的子句集。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 需說明的是，在上述求子句集的過程中，當(dāng)消去存在量詞后，把所有全稱量詞都依次移到整個(gè)式子的最左邊（或者先把所有量詞都依次移到整個(gè)式子的最左邊，再消去存在量詞），再將右部的式子化為合取范式，這時(shí)所得的式子稱為原公式的稱為Skolem標(biāo)準(zhǔn)型。例如，上例中謂詞公式的Skole

22、m標(biāo)準(zhǔn)型就是 x乛P(x,f(x)Q(x,g(x)乛P(y,f(y)乛R(y,g(y)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.8 設(shè)G=xyzuvw(P(x,y,z)Q(u,v,w)，那么，用a代替x，用f(y,z)代替u，用g(y,z,v)代替w，則得G的Skolem標(biāo)準(zhǔn)型 y z v(P(a,y,z)乛Q(f(y,z),v,g(y,z,v) 進(jìn)而得G的子句集為 P(a,x,y),乛Q(f(u,v),w,g(u,v,w) 由此例還可看出，一個(gè)公式的子句集也可以通過先求前束范式，再求Skolem標(biāo)準(zhǔn)型而得到。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)

23、器推理 ( )( )(0)(1)0,1 ,0GxP xGP aa PPDFT 它的Skolem標(biāo)準(zhǔn)型是我們給出如下的一個(gè)解釋I： 需說明的是，引入Skolem函數(shù)，是由于存在量詞在全稱量詞的轄域之內(nèi)，其約束變?cè)娜≈祫t完全依賴于全稱量詞的取值。Skolem函數(shù)就反映了這種依賴關(guān)系。但注意，Skolem標(biāo)準(zhǔn)型與原公式一般并不等價(jià)，例如有公式：則在I下, G=T, 而G=F。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定理定理1 把證明一個(gè)公式G的不可滿足性，轉(zhuǎn)化為證明其子句集S的不可滿足性。 定義定義3 子句集S是不可滿足的，當(dāng)且僅當(dāng)其全部子句的合取式是不可滿足的。第第5 5

24、章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.2.2 命題邏輯中的歸結(jié)原理命題邏輯中的歸結(jié)原理 歸結(jié)演繹推理是基于一種稱為歸結(jié)原理(亦稱消解原理principleofresolution)的推理規(guī)則的推理方法。歸結(jié)原理是由魯濱遜(J.A.Robinson)于1965年首先提出。它是謂詞邏輯中一個(gè)相當(dāng)有效的機(jī)械化推理方法。歸結(jié)原理的出現(xiàn)，被認(rèn)為是自動(dòng)推理，特別是定理機(jī)器證明領(lǐng)域的重大突破。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義4 設(shè)L為一個(gè)文字，則稱L與L為互補(bǔ)文字。 定義定義5 設(shè)C1,C2是命題邏輯中的兩個(gè)子句，C1中有文字L1，C2中有文字L2，且

25、L1與L2互補(bǔ)，從C1,C2中分別刪除L1,L2，再將剩余部分析取起來，記構(gòu)成的新子句為C12，則稱C12為C1,C2的歸結(jié)式(或消解式)，C1,C2稱為其歸結(jié)式的親本子句， L1,L2稱為消解基。 例例3.9 設(shè)C1=乛PQR,C2=乛QS,于是C1,C2的歸結(jié)式為乛PRS 定理2 歸結(jié)式是其親本子句的邏輯結(jié)果。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 證明 設(shè)C1=LC1,C2=乛LC2,C1,C2都是文字的析取式，則C1,C2的歸結(jié)式為C1C2，因?yàn)?C1=C1L=乛(C1L),C2=LC2=(LC2)所以 C1C2=(乛C1L)(LC2)乛(C1C2)=C1C2 證

26、畢。 由定理2即得推理規(guī)則： C1C2 (C1-L1)(C2-L2) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.10 用歸結(jié)原理驗(yàn)證分離規(guī)則：A(AB) B和拒取式(AB)乛B 乛A。 解 A(AB) A(乛AB)B (AB)乛B (乛AB)(乛B) 乛A 類似地可以驗(yàn)證其他推理規(guī)則也都可以經(jīng)消解原理推出。這就是說，用消解原理就可以代替其他所有的推理規(guī)則。再加上這個(gè)方法的推理步驟比較機(jī)械，這就為機(jī)器推理提供了方便。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 推論 設(shè)C1,C2是子句集S的兩個(gè)子句，C12是它們的歸結(jié)式，則 (1)若用C12代替C1,

27、C2，得到新子句集S1，則由S1的不可滿足可推出原子句集S的不可滿足。即 S1不可滿足 S不可滿足 (2)若把C12加入到S中，得到新子句集S2，則S2與原S的同不可滿足。即 S2不可滿足 S不可滿足第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.11 證明子句集PQ,P,Q是不可滿足的。證證(1)P乛Q(2)乛P(3)Q(4)乛Q 由(1),(2)(5) 由(3),(4)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.12 用歸結(jié)原理證明R是P,(PQ)R,(SU)Q,U的邏輯結(jié)果。 證 我們先把諸前提條件化為子句形式，再把結(jié)論的非也化為子句，由所

28、有子句得到子句集S=P,乛P乛QR,乛SQ,乛UQ,U,乛R，然后對(duì)該子句集施行歸結(jié)，歸結(jié)過程用下面的歸結(jié)演繹樹表示（見圖31）。由于最后推出了空子句，所以子句集S不可滿足，即命題公式 P(乛P乛QR)(乛SQ)(乛UQ)U乛R 不可滿足，從而R是題設(shè)前提的邏輯結(jié)果。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 圖51 例5.12歸結(jié)演繹樹 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.2.3 替換與合一替換與合一 在一階謂詞邏輯中應(yīng)用消解原理，不像命題邏輯中那樣簡(jiǎn)單，因?yàn)橹^詞邏輯中的子句含有個(gè)體變?cè)?，這就使尋找含互否文字的子句對(duì)的操作變得復(fù)雜。例如： C

29、1=P(x)Q(x) C2=P(a)R(y) 直接比較，似乎兩者中不含互否文字，但如果我們用a替換C1中的x，則得到 C1=P(a)Q(a) C2=P(a)R(y)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 于是根據(jù)命題邏輯中的消解原理，得C1和C2的消解式 C3=Q(a)R(y) 所以，要在謂詞邏輯中應(yīng)用消解原理，則一般需要對(duì)個(gè)體變?cè)鬟m當(dāng)?shù)奶鎿Q。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義6 一個(gè)替換(Substitution)是形如t1/x1,t2/x2,tn/xn的有限集合，其中t1,t2,tn是項(xiàng)，稱為替換的分子；x1,x2,xn是互不相同

30、的個(gè)體變?cè)?，稱為替換的分母；ti不同于xi，xi也不循環(huán)地出現(xiàn)在tj(i,j=1,2,n)中；ti/xi表示用ti替換xi。若t1,t2,tn都是不含變?cè)捻?xiàng)（稱為基項(xiàng)）時(shí)，該替換稱為基替換；沒有元素的替換稱為空替換，記作，它表示不作替換。例如：第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 a/x,g(y)/y , f(g(b)/z就是一個(gè)替換，而g(y)/x, f(x)/y則不是一個(gè)替換,因?yàn)閤與y出現(xiàn)了循環(huán)替換。下面我們將項(xiàng)、原子公式、文字、子句等統(tǒng)稱為表達(dá)式，沒有變?cè)谋磉_(dá)式稱為基表達(dá)式，出現(xiàn)在表達(dá)式E中的表達(dá)式稱為E的子表達(dá)式。 定義定義7 設(shè)=t1/x1,tn/xn是

31、一個(gè)替換，E是一個(gè)表達(dá)式，把對(duì)E施行替換，即把E中出現(xiàn)的個(gè)體變?cè)獂j(1jn)都用tj替換，記為E，所得的結(jié)果稱為E在下的例(instance)。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義8 設(shè)=t1/x1,tn/xn,=u1/y1,um/ym是兩個(gè)替換，則將集合 t1/x1,tn/xn,u1/y1,um/ym 中凡符合下列條件的元素刪除： (1)ti/xi 當(dāng)ti=xi (2)ui/yi當(dāng)yix1,xn 如此得到的集合仍然是一個(gè)替換，該替換稱為與的復(fù)合或乘積，記為。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.13 設(shè)=f(y)/x,z

32、/y =a/x,b/y,y/z于是, t1/x1,t2/x2,u1/y1,u2/y2,u3/y3=f(b)/x,y/ y,a/x,b/y,y/z從而=f(b)/x,y/z可以證明，替換的乘積滿足結(jié)合律，即 ()u=(u)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義9 設(shè)S=F1,F2,Fn是一個(gè)原子謂詞公式集，若存在一個(gè)替換，可使F1=F2=Fn，則稱為S的一個(gè)合一(Unifier)，稱S為可合一的。 一個(gè)公式集的合一一般不唯一。 定義10 設(shè)是原子公式集S的一個(gè)合一，如果對(duì)S的任何一個(gè)合一，都存在一個(gè)替換，使得 = 則稱為S的最一般合一(MostGeneralUni

33、fier)，簡(jiǎn)稱MGU。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.14 設(shè)S=P(u,y,g(y),P(x,f(u),z)，S有一個(gè)最一般合一 =u/x,f(u)/y,g(f(u)/z 對(duì)S的任一合一，例如： =a/x,f(a)/y,g(f(a)/z,a/u 存在一個(gè)替換 =a/u 使得 =第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，如果能找到一個(gè)公式集的合一，特別是最一般合一，則可使互否的文字的形式結(jié)構(gòu)完全一致起來，進(jìn)而達(dá)到消解的目的。如何求一個(gè)公式集的最一般合一？有一個(gè)算法，可以求任何可合一公式集的最一般合一。為了介紹這個(gè)算法，我們

34、先引入差異集的概念。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義11 設(shè)S是一個(gè)非空的具有相同謂詞名的原子公式集，從S中各公式的左邊第一個(gè)項(xiàng)開始，同時(shí)向右比較，直到發(fā)現(xiàn)第一個(gè)不都相同的項(xiàng)為止，用這些項(xiàng)的差異部分組成一個(gè)集合，這個(gè)集合就是原公式集S的一個(gè)差異集。 例例3.15 設(shè)S=P(x,y,z),P(x,f(a),h(b)，則不難看出，S有兩個(gè)差異集 D1=y,f(a) D2=z,h(b) 設(shè)S為一非空有限具有相同謂詞名的原子謂詞公式集，下面給出求其最一般合一的算法。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 合一算法合一算法(Unificati

35、on algorithm)：步步1 置k=0, Sk=S，k=;步步2 若Sk只含有一個(gè)謂詞公式，則算法停止，k就是要 求的最一般合一;步步3 求Sk的差異集Dk;步步4 若Dk中存在元素xk和tk，其中xk是變?cè)?，tk是項(xiàng)且xk 不在tk中出現(xiàn)，則置Sk +1= Sk tk/xk,k+1=ktk/xk，k=k+1，然后轉(zhuǎn)步2;步步5 算法停止，S的最一般合一不存在。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.16 求公式集S=P(a,x,f(g(y),P(z,h(z,u),f(u)的最一般合一。 解解 k=0： S0=S, 0=,S0不是單元素集，求得D0=a,z，

36、其中z是變?cè)?，且不在a中出現(xiàn)，所以有 1=0a/z=a/z=a/zS1=S0a/z=P(a,x,f(g(y),P(a,h(a,u),f(u) k=1: S1不是單元素集，求得D1=x,h(a,u)， 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 所以2=1h(a,u)/x=a/zh(a,u)/x=a/u,h(a,u)/xS2=S1h(a,u)/x=P(a,h(a,u),f(g(y),P(a,h(a,u),f(u)k=2:S2不是單元素集，D2=g(y),u，3=2g(y)/u=a/z,h(a,g(y)/x,g(y)/uS3=S2g(y)/u=P(a,h(a,g(y),f(g(y

37、),P(a,h(a,g(y),f(g(y)=P(a,h(a,g(y),f(g(y)k=3:S3已是單元素集，所以3就是S的最一般合一。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.17 判定S=P(x,x),P(y,f(y)是否可合一？解解k=0:S0=S,0=,S0不是單元素集，D0=x,y1=0y/x=y/xS1=S0y/x=P(y,y),P(y,f(y)k=1:第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 S1不是單元素集，D1=y,f(y)，由于變?cè)獃在項(xiàng)f(y)中出現(xiàn)，所以算法停止，S不存在最一般合一。 從合一算法可以看出，一個(gè)公式集S的最一般

38、合一可能是不唯一的，因?yàn)槿绻町惣疍k=ak,bk，且ak和bk都是個(gè)體變?cè)?，則下面兩種選擇都是合適的： k+1=kbk/ak或k+1=kak/bk第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定理定理3 （合一定理）如果S是一個(gè)非空有限可合一的公式集，則合一算法總是在步2停止，且最后的k即是S的最一般合一。本定理說明任一非空有限可合一的公式集，一定存在最一般合一，而且用合一算法總能找到最一般合一，這個(gè)最一般合一也就是當(dāng)算法終止在步2時(shí)，最后的合一k。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 3.2.4 謂詞邏輯中的歸結(jié)原理謂詞邏輯中的歸結(jié)原理 定義定義12

39、 設(shè)C1,C2是兩個(gè)無相同變?cè)淖泳?，L1,L2分別是C1,C2中的兩個(gè)文字，如果L1和L2有最一般合一，則子句(C1-L1)(C2-L2)稱作C1和C2的二元?dú)w結(jié)式(二元消解式)，C1和C2稱作歸結(jié)式的親本子句，L1和L2稱作消解文字。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.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(

40、y) 所以，Q(a)R(y)是C1和C2的二元?dú)w結(jié)式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.19 設(shè)C1=P(x,y)Q(a),C2=Q(x)R(y),求C1,C2的歸結(jié)式。 解解 由于C1,C2中都含有變?cè)獂,y，所以需先對(duì)其中一個(gè)進(jìn)行改名,方可歸結(jié)（歸結(jié)過程是顯然的，故從略）。還需說明的是，如果在參加歸結(jié)的子句內(nèi)部含有可合一的文字，則在進(jìn)行歸結(jié)之前，也應(yīng)對(duì)這些文字進(jìn)行合一，從而使子句達(dá)到最簡(jiǎn)。例如，設(shè)有兩個(gè)子句： C1=P(x)P(f(a)Q(x) C2=P(y)R(b)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可見,在C1中有可合一的

41、文字P(x)與P(f(a)，那么，取替換=f(a)/x(這個(gè)替換也就是P(x)和P(f(a)的最一般合一)，則得 C1=P(f(a)Q(f(a) 現(xiàn)在再用C1與C2進(jìn)行歸結(jié)，從而得到C1與C2的歸結(jié)式 (f(a)R(b) 定義定義13 如果子句C中，兩個(gè)或兩個(gè)以上的文字有一個(gè)最一般合一，則C稱為C的因子，如果C是單元子句，則C稱為C的單因子。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.20 設(shè)C=P(x)P(f(y)乛Q(x),令=f(y)/x，于是C=P(f(y)乛Q(f(y)是C的因子。 定義定義14 子句C1,C2的消解式，是下列二元消解式 之一： (1)C1

42、和C2的二元消解式; (2)C1和C2的因子的二元消解式; (3)C1的因子和C2的二元消解式; (4)C1的因子和C2的因子的二元消解式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定理定理4 謂詞邏輯中的消解式是它的親本子句的邏輯結(jié)果。(證明類似于定理2，故從略。) 由此定理我們即得謂詞邏輯中的推理規(guī)則： C1C2 (C1-L1)(C2-L2) 其中C1,C2是兩個(gè)無相同變?cè)淖泳?，L1,L2分別是C1,C2中的文字，為L(zhǎng)1與L2的最一般合一。此規(guī)則稱為謂詞邏輯中的消解原理（或歸結(jié)原理）。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.21 求證

43、G是A1和A2的邏輯結(jié)果。A1: x(P(x)(Q(x)R(x)A2: x(P(x)S(x)G: x(S(x)R(x) 證證 我們用反證法，即證明A1A2乛G不可滿足。首先求得子句集S： 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (1)乛P(x)Q(x) (2)乛P(y)R(y) (3)P(a) (4)S(a) (5)乛S(z)乛R(z)(乛G) 然后應(yīng)用消解原理，得(6)R(a) (2),(3),1=a/y(7)乛R(a) (4),(5),2=a/z(8) (6),(7)所以S是不可滿足的，從而G是A1和A2的邏輯結(jié)果。 (A1) (A2) S第第5 5章章 基于謂詞邏輯

44、的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.22 設(shè)已知：(1)能閱讀者是識(shí)字的；(2)海豚不識(shí)字；(3)有些海豚是很聰明的。試證明：有些聰明者并不能閱讀。證 首先，定義如下謂詞：R(x)：x能閱讀。L(x)：x識(shí)字。I(x)：x是聰明的。D(x)：x是海豚。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 然后把上述各語句翻譯為謂詞公式：(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é)論 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 求題設(shè)與結(jié)論否定的子句集，得(1)乛R(x)L

45、(x)(2)乛D(y)乛L(y)(3)D(a)(4)I(a)(5)乛I(z)R(z)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 歸結(jié)得(6) R(a) (5)，(4)，a/z(7) L (a) (6)，(1)，a/x(8) 乛D(a) (7), (2), a/y(9) (8), (3)這個(gè)歸結(jié)過程的演繹樹如圖32所示。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 由以上例子可以看出，謂詞邏輯中的消解原理也可以代替其他推理規(guī)則。 上面我們通過推導(dǎo)空子句，證明了子句集的不可滿足性，于是存在問題：對(duì)于任一不可滿足的子句集，是否都能通過歸結(jié)原理推出空子句呢？回答是肯

46、定的。 定理定理5 （歸結(jié)原理的完備性定理）如果子句集S是不可滿足的，那么必存在一個(gè)由S推出空子句的消解序列。(該定理的證明要用到Herbrand定理，故從略。) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 圖5-2 例3.22 歸結(jié)演繹樹 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 歸結(jié)原理除了能用于對(duì)已知結(jié)果的證明外，還能用于對(duì)未知結(jié)果的求解，即能求出問題的答案來。請(qǐng)看下例。 例例3.23 已知: (1)如果x和y是同班同學(xué)，則x的老師也是y的老師。 (2)王先生是小李的老師。 (3)小李和小張是同班同學(xué)。 問：小張的老師是誰？ 5.3 應(yīng)用歸結(jié)原理求取

47、問題答案應(yīng)用歸結(jié)原理求取問題答案第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 解解 設(shè)謂詞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) 為了得到問題的答案，我們先證明小張的老師是存在的，即證明公式： G: x T(x,Zhang) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 于是，求F1F2F3 G的子句集如下:(1) C(x,y) T(z,x)T(z,y)(2)T(Wang,Li)(3)C(Li

48、,Zhang)(4) T(u,Zhang)歸結(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) 由(3),(6)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 這說明，小張的老師確實(shí)是存在的。那么，為了找到這位老師，我們給原來的求證謂詞的子句再增加一個(gè)謂詞ANS(u)。于是，得到 (4) T(u,Zhang)ANS(u)現(xiàn)在，我們用(4)代替(4)，重新進(jìn)行歸結(jié)，則得 (5) C(Li,y)T(Wang,y) 由(1)(2) (6) C(Li,Zhang)

49、ANS(Wang) 由(4)(5) (7)ANS(Wang) 由(3)(6) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，歸結(jié)到這一步，求證的目標(biāo)謂詞已被消去，即求證已成功，但還留下了謂詞ANS(Wang)。由于該謂詞中原先的變?cè)c目標(biāo)謂詞T(u,Zhang)中的一致，所以，其中的Wang也就是變?cè)猽的值。這樣，我們就求得了小張的老師也是王老師。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 上例雖然是一個(gè)很簡(jiǎn)單的問題，但它給了我們一個(gè)利用歸結(jié)原理求取問題答案的方法，那就是：先為待求解的問題找一個(gè)合適的求證目標(biāo)謂詞；再給增配（以析取形式）一個(gè)輔助謂詞，

50、且該輔助謂詞中的變?cè)仨毰c對(duì)應(yīng)目標(biāo)謂詞中的變?cè)耆恢?；然后進(jìn)行歸結(jié)，當(dāng)某一步的歸結(jié)式剛好只剩下輔助謂詞時(shí)，輔助謂詞中原變?cè)恢蒙系捻?xiàng)（一般是常量）就是所求的問題答案。需說明的是，輔助謂詞（如此題中的ANS）是一個(gè)形式謂詞，其作用僅是提取問題的答案，因而也可取其他謂詞名。有些文獻(xiàn)中就用需求證的目標(biāo)謂詞。如對(duì)上例，就取T(u,Zhang)為輔助謂詞。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.24 設(shè)有如下關(guān)系:(1)如果x是y的父親，y又是z的父親，則x是z的祖父。(2)老李是大李的父親。(3)大李是小李的父親。問：上述人員中誰和誰是祖孫關(guān)系？解 先把上述前提中的三個(gè)

51、命題符號(hào)化為謂詞公式：F1: x y z(F(x,y)F(y,z)G(x,z)F2: F(Lao,Da)F3: F(Da,Xiao) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 并求其子句集如下:(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的祖父) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 把其否定化為子句形式再析取一個(gè)輔助謂詞GA(x,y)，得 (4)乛G(u,v)GA(u,v) 對(duì)(1)(4)進(jìn)行歸結(jié),得 (5)乛F(Da,z)G(

52、Lao,z) (1),(2),Lao/x,Da/y (6)G(Lao,Xiao) (3),(5),Xiao/z (7)GA(Lao,Xiao) (4),(6),Lao/u,Xiao/v 所以，上述人員中，老李是小李的祖父。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.4.1 問題的提出問題的提出 前面我們介紹了歸結(jié)原理及其應(yīng)用，但前面的歸結(jié)推理都是用人工實(shí)現(xiàn)的。而人們研究歸結(jié)推理的目的主要是為了更好地實(shí)現(xiàn)機(jī)器推理，或者說自動(dòng)推理。那么，現(xiàn)在就存在問題：歸結(jié)原理如何在機(jī)器上實(shí)現(xiàn)？把歸結(jié)原理在機(jī)器上實(shí)現(xiàn)，就意味著要把歸結(jié)原理用算法表示，然后編制程序，在計(jì)算機(jī)上運(yùn)行。下面我們給出

53、一個(gè)實(shí)現(xiàn)歸結(jié)原理的一般性算法： 5.4 歸結(jié)策略歸結(jié)策略第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 步1 將子句集S置入CLAUSES表； 步2 若空子句NIL在CLAUSES中，則歸結(jié)成功，結(jié)束。 步3 若CLAUSES表中存在可歸結(jié)的子句對(duì)，則歸結(jié)之，并將歸結(jié)式并入CLAUSES表，轉(zhuǎn)步2； 步4 歸結(jié)失敗，退出。 可以看出，這個(gè)算法并不復(fù)雜，但問題是在其步3中應(yīng)該以什么樣的次序從已給的子句集S出發(fā)尋找可歸結(jié)的子句對(duì)而進(jìn)行歸結(jié)呢？第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 一種簡(jiǎn)單而直接的想法就是逐個(gè)考察CLAUSES表中的子句，窮舉式地進(jìn)行歸結(jié)?？刹捎?/p>

54、這樣的具體作法：第一輪歸結(jié)先讓CLAUSES表(即原子句集S)中的子句兩兩見面進(jìn)行歸結(jié)，將產(chǎn)生的歸結(jié)式集合記為S1，再將S1并入CLAUSES得CLAUSESSS1；下一輪歸結(jié)時(shí)，又讓新的CLAUSES即SS1與S1中的子句互相見面進(jìn)行歸結(jié)，并把產(chǎn)生的歸結(jié)式集合記為S2，再將S2并入CLAUSES；再一輪歸結(jié)時(shí)，又讓SS1S2與S2中的子句進(jìn)行歸結(jié)如此進(jìn)行，直到某一個(gè)Sk中出現(xiàn)空子句為止。下面我們舉例。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.25 設(shè)有如下的子句集S，我們用上述的窮舉算法歸結(jié)如下： S: (1)PQ (2)乛PQ (3)P乛Q (4)乛P乛Q S

55、1:(5)Q (1),(2) (6)P (1),(3) (7)Q乛Q (1),(4) (8)P乛P (1),(4) (9)Q乛Q (2),(3) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (10)P乛P (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),(11) (18)P (1),(12) (19)Q (2),(6) (20)乛PQ (2),(7)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器

56、推理 (21)乛PQ (2),(8)(22)乛PQ (2),(9)(23)乛PQ (2),(10)(24)乛P (2),(12)(25)P (3),(5)(26)P乛Q (3),(7)(27)P乛Q (3),(8)(28)P乛Q (3),(9)(29)P乛Q (3),(10)(30)乛Q (3),(11)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (31)乛P (4),(5)(32)乛Q (4),(6)(33)乛P乛Q (4),(7)(34)乛P乛Q (4),(8)(35)乛P乛Q (4),(9)(36)乛P乛Q (4),(10)(37)Q (5),(7)(38)Q (5),

57、(9)(39) (5),(12)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，這個(gè)歸結(jié)方法無任何技巧可言，只是一味地窮舉式歸結(jié)。因而對(duì)于如此簡(jiǎn)單的問題，計(jì)算機(jī)推導(dǎo)了35步，即產(chǎn)生35個(gè)歸結(jié)式，才導(dǎo)出了空子句。那么，對(duì)于一個(gè)規(guī)模較大的實(shí)際問題，其時(shí)空開銷就可想而知了。事實(shí)上，這種方法一般會(huì)產(chǎn)生許多無用的子句。這樣，隨著歸結(jié)的進(jìn)行，CLAUSES表將會(huì)越來越龐大，以至于機(jī)器不能容納。同時(shí)，歸結(jié)的時(shí)間消耗也是一個(gè)嚴(yán)重問題。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.4.2 幾種常用的歸結(jié)策略幾種常用的歸結(jié)策略 1.刪除策略刪除策略 定義 設(shè)C1,C2

58、是兩個(gè)子句，若存在替換，使得C1C2，則稱子句C1類含C2。 例如： P(x)類含P(a)Q(y) (只需取=a/x) Q(y)類含P(x)Q(y) (=) P(x)類含P(x),P(x)類含P(a),P類含P,P類含PR P(a,x)P(y,b)類含P(a,b) (取=b/x,a/y) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 刪除策略： 在歸結(jié)過程中可隨時(shí)刪除以下子句： (1)含有純文字的子句； (2)含有永真式的子句； (3)被子句集中別的子句類含的子句。 所謂純文字，是指那些在子句集中無補(bǔ)的文字。例如下面的子句集 P(x)Q(x,y)R(x),P(a)Q(u,v),

59、Q(b,z),P(w)中的文字R(x)就是一個(gè)純文字。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 刪除含有純文字的子句，是因?yàn)樵跉w結(jié)時(shí)純文字永遠(yuǎn)不會(huì)被消去，因而用包含它的子句進(jìn)行歸結(jié)不可能得到空子句。刪除永真式是因?yàn)橛勒媸綄?duì)子句集的不可滿足性不起任何作用。刪除被類含的子句是因?yàn)楸活惡泳浔活惡淖泳渌壿嬏N(yùn)含，故它已是多余的。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.26 我們?cè)诶?.25中使用刪除策略?？梢钥闯觯@時(shí)原歸結(jié)過程中產(chǎn)生的有些歸結(jié)式是永真式（如(7)、(8)、(9)、(10)），有些被前面已有的子句所類含（如(17)、(18)等，

60、重復(fù)出現(xiàn)可認(rèn)為是一種類含），因此，它們可被立即刪除。這樣就導(dǎo)致它們的后裔將不可能出現(xiàn)。于是，歸結(jié)步驟可簡(jiǎn)化為 (1)PQ (2)乛PQ (3)P乛Q (4)乛P乛Q第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (5)Q (1),(2)(6)P (1),(3)(7)乛P (2),(4)(8)乛Q (3),(4)(9) (5),(8)其實(shí)，上述歸結(jié)還可以進(jìn)一步簡(jiǎn)化為(5)Q (1),(2)(6)乛Q (3),(4)(7) (5),(6) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.27 對(duì)下面的子句集S，我們用寬度優(yōu)先策略與刪除策略相結(jié)合的方法進(jìn)行消解。