人工智能原理02章 歸結(jié)推理方法23 謂詞邏輯歸結(jié)法基礎(chǔ)

1、2.3 謂詞邏輯歸結(jié)法基礎(chǔ)由于謂詞邏輯與命題邏輯不同，有量詞、變量和函數(shù)，所以在生成子句集之前要對邏輯公式做處理，具體的說就是要將其轉(zhuǎn)化為Skolem標(biāo)準(zhǔn)形，然后在子句集的基礎(chǔ)上再進(jìn)行歸結(jié)，雖然基本的歸結(jié)的基本方法都相同，但是其過程較之命題公式的歸結(jié)過程要復(fù)雜得多。本節(jié)針對謂詞邏輯歸結(jié)法介紹了Skolem標(biāo)準(zhǔn)形、子句集等一些必要的概念和定理。 231 Skolem 標(biāo)準(zhǔn)形Skolem標(biāo)準(zhǔn)形的定義：前束范式中消去所有的存在量詞，則稱這種形式的謂詞公式為Skolem標(biāo)準(zhǔn)形，任何一個(gè)謂詞公式都可以化為與之對應(yīng)的Skolem標(biāo)準(zhǔn)形。但是，Skolem標(biāo)準(zhǔn)形不唯一。 前束范式：A是一個(gè)前束范式，如果A中

2、的一切量詞都位于該公式的最左邊（不含否定詞），且這些量詞的轄域都延伸到公式的末端。 Skolem標(biāo)準(zhǔn)形的轉(zhuǎn)化過程為，依據(jù)約束變量換名規(guī)則，首先把公式變型為前束范式，然后依照量詞消去原則消去或者略去所有量詞。具體步驟如下： 將謂詞公式G轉(zhuǎn)換成為前束范式前束范式的形式為：(Q1x1)(Q2x2)(Qnxn)M(x1,x2,xn)即： 把所有的量詞都提到前面去。注意：由于所有的量詞的轄域都延伸到公式的末端，即，最左邊量詞將約束表達(dá)式中的所有同名變量。所以將量詞提到公式最前端時(shí)存在約束變量換名問題。要嚴(yán)守規(guī)則。 約束變量換名規(guī)則：(Qx ) M（x） （Qy ） M（y） (Qx ) M（x,z） （

3、Qy ） M（y,z）量詞否定等值式：(x ) M（x） （y ） M（y） (x ) M（x） （y ） M（y）量詞分配等值式：(x )( P（x） Q（x）) (x ) P（x） (x ) Q（x）(x )( P（x） Q（x）) (x ) P（x） (x ) Q（x）消去量詞等值式：設(shè)個(gè)體域?yàn)橛懈F集合（a1, a2, an）(x ) P（x） P（a1） P（a2） P（an）(x ) P（x） P（a1） P（a2） P（an）量詞轄域收縮與擴(kuò)張等值式：( x )( P（x） Q) ( x ) P（x） Q(x )( P（x） Q) ( x ) P（x） Q (x )( P（x） Q

4、) (x ) P（x） Q (x )( Q P（x） ) Q (x ) P（x） (x )( P（x） Q) (x ) P（x） Q(x )( P（x） Q) (x ) P（x） Q (x )( P（x） Q) (x ) P（x） Q (x )( Q P（x） ) Q (x ) P（x）消去量詞量詞消去原則：1) 消去存在量詞""，即，將該量詞約束的變量用任意常量（a, b等）、或全稱變量的函數(shù)(f(x), g(y)等)代替。如果存在量詞左邊沒有任何全稱量詞，則只將其改寫成為常量；如果是左邊有全程量詞的存在量詞，消去時(shí)該變量改寫成為全程量詞的函數(shù)。 2) 略去全程量詞&qu

5、ot;"，簡單地省略掉該量詞。Skolem 定理：謂詞邏輯的任意公式都可以化為與之等價(jià)的前束范式，但其前束范式不唯一。 注意：公式G的SKOLEM標(biāo)準(zhǔn)形同G并不等值。例題2-2將下式化為Skolem標(biāo)準(zhǔn)形：(x)(y)P(a, x, y) (x)(y)Q(y, b)R(x)解：第一步，消去號，得：(x)(y)P(a, x, y) (x) (y)Q(y, b)R(x)第二步，深入到量詞內(nèi)部，得：(x)(y)P(a, x, y)(x) (y)Q(y, b)R(x) (x)(y)P(a, x, y) (x) (y)Q(y, b)R(x)第三步，全稱量詞左移，（利用分配律），得(x)( (y

6、)P(a, x, y) (y)(Q(y, b)R(x)第四步，變元易名，存在量詞左移，直至所有的量詞移到前面，得：(x)( (y)P(a, x, y) (y)(Q(y, b)R(x) (x) ( (y)P(a, x, y) (z)(Q(z, b)R(x)= (x) (y) (z) (P(a, x, y) Q(z, b)R(x)由此得到前述范式第五步，消去""（存在量詞），略去""全稱量詞消去(y)，因?yàn)樗筮呏挥?"x)，所以使用x的函數(shù)f(x)代替之，這樣得到：(x)(z)( P(a, x, f(x) Q(z, b)R(x)消去(z)，同理使

7、用g(x)代替之，這樣得到：(x) ( P(a, x, f(x) Q(g(x), b)R(x)則，略去全稱變量，原式的Skolem標(biāo)準(zhǔn)形為：P(a, x, f(x) Q(g(x), b)R(x)2.3.2子句集文字：不含任何連接詞的謂詞公式。子句：一些文字的析?。ㄖ^詞的和）。子句集：所有子句的集合對于任一個(gè)公式G，都可以通過Skolem標(biāo)準(zhǔn)形，標(biāo)準(zhǔn)化建立起一個(gè)子句集與之相對應(yīng)。因?yàn)樽泳洳贿^是一些文字的析取，是一種比較簡單的形式，所以對G的討論就用對子句集S的討論來代替，以便容易處理。 子句集S可由下面的步驟求?。?. 謂詞公式G轉(zhuǎn)換成前束范式2. 消去前束范式中的存在變量，略去其中的任意變量，

8、生成SKOLEM標(biāo)準(zhǔn)形3. 將SKOLEM標(biāo)準(zhǔn)形中的各個(gè)子句提出，表示為集合形式 教師提示：為了簡單起見，子句集生成可以理解為是用"，"取代SKOLEM標(biāo)準(zhǔn)形中的""，并表示為集合形式 。注意：SKOLEM標(biāo)準(zhǔn)形必須滿足合取范式的條件。即，在生成子句集之前邏輯表達(dá)式必須是各"謂詞表達(dá)式"或"謂詞或表達(dá)式"的與。定理謂詞表達(dá)式G是不可滿足的當(dāng)且僅當(dāng) 其子句集S是不可滿足的公式G與其子句集S并不等值，但它們在不可滿足的意義下是一致的。因此如果要證明A1A2A3B，只需證明G A1A2A3B的子句集是不可滿足的，這也正是

9、引入子句集的目的。 注意：公式G和子句集S雖然不等值，但是它們的之間一般邏輯關(guān)系可以簡單的說明為：G真不一定S真，而S真必有G真，即，S G。在生成SKOLEM標(biāo)準(zhǔn)形時(shí)將存在量詞用常量或其他變量的函數(shù)代替，使得變量討論的論域發(fā)生了變化，即論域變小了。所以G不能保證S真。定理的推廣對于形如G = G1 G2 G3 Gn 的謂詞公式，G的子句集的求取過程可以分解成幾個(gè)部分單獨(dú)處理。如果Gi的子句集為Si，則有 S' = S1 S2 S3 Sn，雖然G的子句集不為S'，但是可以證明：SG 與S1 S2 S3 Sn在不可滿足的意義上是一致的。即SG 不可滿足 S1 S2 S3 Sn不可

10、滿足由上面的定理，我們對SG的討論，可以用較為簡單的S1 S2 S3 Sn來代替。為方便起見，也稱S1 S2 S3 Sn為G的子句形，即：SGS1 S2 S3 Sn。根據(jù)以上定理可對一個(gè)謂詞表達(dá)式分而治之，化整為零，大大減少了計(jì)算復(fù)雜度。 例23對所有的x,y,z來說，如果y是x的父親，z又是y的父親，則z是x的祖父。又知每個(gè)人都有父親，試問對某個(gè)人來說誰是它的祖父？用一階邏輯表示這個(gè)問題，并建立子句集。解：這里我們首先引入謂詞：P(x, y) 表示x是y的父親Q(x, y) 表示x是y的祖父ANS(x) 表示問題的解答于是有：對于第一個(gè)條件，"如果y是x的父親，z又是y的父親，則z是x的祖父"，一階邏輯表達(dá)式如下：A1：(x)(y)(z)(P(x, y)P(y, z)Q(x, z)則把A1化為合取范式，進(jìn)而化為Skolem標(biāo)準(zhǔn)形，表示如下：S A1：P(x ,y)P(y, z)Q(x, z)對于