一阶逻辑的推论

第九章一階邏輯的推論9.1包含量詞的推論規則9.2一個證明範例9.3一般化的Modus法9.4向前與向後連鎖9.5完備性9.6解析:一個完備的推論程序9.7解析的完備性本章我們將定義可以利用一階邏輯很有效率的回答問題的推論機制。9.1包含量詞的推論規則在6.4節，我們看到了命題邏輯的推論規則：Modus法、And-消去法、And引入、Or-引入以及解析法。這些規則對於一階邏輯一樣成立。但是我們需要額外的推論規則處理具有量詞的一階邏輯命題。我們在這裡將介紹三個新的命題規則，它們將比前面的困難一些，因為我們必須討論有關於變數的特別個體的取代。我們將使用SUBST(,)這個符號表示應用取代（或連結清單）

在命題

的結果。新的推論規則如下：全體性消去：對於任何命題，變數以及基礎項目g存在性消去：對於任何命題，變數以及沒有出現在知識庫其他地方的常數符號k

存在性引入：對於任何命題，沒有出現在命題中的變數，以及出現在命題中的基礎項目g9.2一個證明範例已經定義了一些推論規則，現在我們說明如何利用它們進行證明。在這裡，對於真實的證明程序指示簡短的步驟，因為推論規則的應用是一個簡單的匹配它們的前題樣式與KB之中的命題的問題，之後加上它們的（適當例子）結論樣式。(課本P8-4~P8-6)這個例子解釋了某些重要的特性：(1)證明共花了14個步驟。(2)分支係數隨著知識庫成長而增加；這是因為某些推論規則組合了存在的論據。整體性消去自己本身可以具有很大的分支係數，因為我們可以用任何的基礎項目取代這一個變數。(3)我們花了許多時間將單元命題組合成連結，舉例說明整體性規則用以匹配，之後應用Modus法。9.3一般化的Modus法

這一節，我們將介紹一般化的Modus推論規則，其將之前需要And-引入、整體性消去及Modus法的證明步驟在一個步驟完成。這個概念能夠取得知識庫的內容，例如：Missile(M1)Owns(Nono,M1)xMissile(x)Owns(Nono,x)

Sell(West,Nono,x)以及一個步驟的推論我們得到Sell(West,Nono,M1)一般性的Modus法是有效率的推論規則共有三個理由：1.它採用了較大的步驟，組合了許多小的推論步驟到一個步驟。2.它採用了合理的步驟──它使用比隨機嘗試整體性消去保證更有置換。這個一致化演算法採用兩個命題並傳回一個使得它們看起來是相同的取代，如果這樣的取代存在的話。3.它利用一個前處理的步驟將在知識庫之中所有的命題轉換成標準形式。將此做一次以及對於所有開始的意思是我們在證明的過程中不必浪費時間在轉換。標準形式

我們試圖用一個推論規則──Modus法的一般化版本──建立推論機制。這指的是，所有在知識庫之中的命題應該是某一種可以匹配Modus法規則某一個前題的形式──否則它們將永遠不會被用到。換句話說，Modus法的標準形式要求在知識庫之中的命題，不是單元命題就是一個以單元命題的連結在式子左邊及一個單元命題在式子右邊的意涵。一致化

一致化函式NUIFY的工作是採取兩個命題p和q並傳回一個置換，使得p和q看起來相同（如果不存在這樣的取代，UNIFY則會傳回失敗）。形式上，UNIFY(p,q)=,其中SUBST(,p)=SUBST(,q)稱為這兩個命題的使一致者。我們將用本文的例子解釋一致化，並將詳細的演算法延至第10章討論。9.4向前與向後連鎖

一般化Modus規則可以用在兩個方面。我們可以從在知識庫之中的命題開始並產生新的結論，其使得我們可以做進一步的推論，這稱為向前連鎖。向前連鎖通常被用在當一個新的命題被加入知識庫，我們想要產生它的推論。另外一種方式，我們可以從我們想要證明的是情開始，找到我們可以下這樣的結論的意涵命題，接著試圖依序建立它的前提。這稱為向後連鎖，因為它將使用向後的Modus法。向前傳遞演算法

向前傳遞演算法通常在一個新的命題p被加入知識庫的時後會被使用。例如，它可以被整合當成是TELL的一部份。這個概念是去尋找所有用p當前提的意涵；之後如果其它的前提還沒有被滿足，我們可已經這個意涵的推論加入知識庫，激發進一步的推論（見圖9.1）向後傳遞演算法

向後傳遞的設計是要對一個在知識庫中提出的問題找到其所有的解答。因此向後傳遞顯示了ASK函式所需的功能。向後傳遞演算法BACK-CHAIN進行的方式是，首先察看它的解答是否可以直接由知識庫之中的的命題得到。之後它找尋所有的意涵，其結論和這個查詢一致，並嘗試建立這些意涵的前提，同樣藉由向後傳遞。如果這些前提是一個連結，則BACK-CHAIN一個部分一個部分處理連結。當所有的前提都找到的時候，對其進行一致化。這一個演算法如圖9.2所示。圖(9.3)是一個證明樹，由命題(9.22)經由(9.30)推導出Criminal(West)。圖9.3也可以看成是向前連鎖的圖。在這一種解釋，前提是被加在底層，而結論將被加入資料庫，當其所有的前提都在資料庫的時候。圖9.4顯示如果在搜尋的過程中做了錯誤的選擇會發稱什麼事──在這個例子，我們選擇美國是一個國家當成問題。9.5

完備性

假設我們有如下的知識庫：x

P(x)Q(x)xP(x)R(x)xQ(x)S(x) (9.40)xR(x)S(x)之後我們想要得到S(A)的結論；S(A)為真如果Q(A)或R(A)為真，同時它們其中的一個應該為真，因為不是P(A)就是P(A)為真。很不幸的，Modus法的連鎖不能為我們推導出S(A)。問題是xP(x)R(x)無法被轉換成Horn形式，因此不能使用Modus法。這樣的意思是表示使用Modus法的推論程序是不完備的：有一些繼承於這個知識庫的命題卻無法被推論出來。如果對於數學敘述的完備性證明程序可以被找到，將會有以下的兩件事情：第一，所有的猜想可以被機械化的建立；第二，所有的數學可以由基礎公設的集合的邏輯推論結果而建立。

9.6解析：一個完備的推論程序

如課本9-21式子，首先，我們可以將它視為依事例而定的推論。如果為偽，則由第一個連結必須為真；但如果為真，則由第二個連結必須為真。因此，或其中有一個必須為真。第二個方式是，將它理解成意涵的遞移：由兩個意涵，我們可以推導出第三個，其連結了第一個意涵的前提與第二個的結論。解析推論規則

在解析規則的簡單形式，前提有剛好兩個連結的部分。我們可以將此推廣成更一般的規則成為兩個任意長度的連結。如果一個連結只有一個子句(pj)和另外一個的連結部分(qk)的否定一致，則推論出所有連結部分的形成的連結除了那兩個之外：

一般化解析（連結）：對於literal文字pi及qi，其中UNIFY(pj,qk)=

一般化解析（意涵）：對於atom單元pi,

qi,

ri,

si,其中UNIFY(pj,qk)=解析的標準形式

在解析規則的第一個版本，每一個命題是一個文字的連結。所有在知識庫中的連結假設成連結成一個很大的隱含的連結(如在一般的KB)，所以這種形式稱之為連結一般形式(Conjunctivenormalform或NCF)，即使每一個個別的命題都是分離（衝突不是嗎？）看出解析就是Modus法的一般化是很重要的。明顯的，意涵一般形式比Horn形式更具有一般性，因為在式子右邊可以是一個分離而不是一個單一的單元。但是乍看之下Modus法有能力組合意涵的單元以一種解析做不到的方式推論出一個新的結論。解析證明

我們可以將解析用在向前連鎖與向後連鎖演算法，如同使用Modus法一樣。圖9.5所示是由在(9.41)的KB得到S(A)的解析證明的三個步驟。

反證法對於整個數學都是一個很有用的工具，而解析方法提供了一個簡單的、健全的、完備的應用方法。圖9.6給了一個這個方法的例子。我們從(9.41)的知識庫開始，並試圖證明S(A)

。我們否定這件事得到S(A)，其在意涵一般形式是S(A)

False，並將它加入知識庫。之後我們應用解析規則直到我們的到矛盾，其在意涵一般形式是TrueFalse。這比圖9.5花了更多的步驟，但是對於證明的完備性這是一個很小的代價。轉換成一般形式

消去意涵：回想p

q

和p

q是相同的。因此，我們將所有的意涵用分離取代。

將向內移：否定在連結一般形式只允許在單元命題，而在意涵一般形式完全不是。我們使用Morgan定律消去範圍較廣的否定（見習題6.2），量詞相等以及雙重否定：(pq) 變成 pq(pq) 變成 pqx,p 變成 xpx,p 變成 xpp 變成 p

變數標準化：對於像(xP(x))(x

Q(x))這樣使用了同一個變數兩次的命題，將其中一個變數的名稱改變。避免我們之後去掉了量詞會發生混淆。量詞左移：命題現在是在一個所有的量詞都可以以它們出現的順序左移的形式，而不會改變命題的意義。

Skolem化：Skolem化是一個藉由消去移動存在性量詞的過程。在這一個簡單的例子，它就像是9.1節的存在性消去規則──將xP(x)轉換成P(A)，其中A

是沒有出現在知識庫其他地方的常數。

對分配：(a

b)

c

變成(a

c)(bc)

平坦巢狀的連結與分離：(a

b)

c變成a

b

c，以及(a

b)

c變成a

b

c。將分離轉換成意涵：隨意的，你可以花一些步驟將命題轉換成意涵一般形式。

證明範例

我們現在將描述如何將轉換程序以及歸謬解析法應用在一個較複雜的例子，這個例子用英文描述是：Jack有一隻狗。每一隻狗的主人都是愛護動物的人。愛護動物的人不會殺害任何的動物。Jack和Curiosity其中有一個人殺了名叫Tuna的貓。Curiosity是否殺了這隻貓？依課本9-29頁解法後，現在的問題是要證明Kills(Curiosity,Tuna)為真。我們假設否定的情形，Kills(Curiosity,Tuna)

False，並應用解析推論規則七次，如圖9.7所示。處理等式

一個處理的方式是公式化等式，藉由描述它們的性質。我們需要說明等式具有反身性、對稱性與遞移性，同時我們也必須說明我們可以取代在任何述詞和函數的等式。因此，我們需要三個基本的公設，以及一個對於每一個述詞及函數：x

x=xx,yx=yy=xx,y,zx=yx=zx=zx,yx=y(P1(x)P1(y))x,yx=y(P2(x)P2(y))

w,x,y,zw=yx=z(F1(w,x)=F1(y,z))w,x,y,zw=yx=z(F2(w,x)=F2(y,z))解調

對於項目x、y和z，其中UNIFY(x,z)=：

x=y,(…z…)(…SUBST(,y)…)如果我們寫下我們所有的等式使得較簡單的項目在式子的右邊（如(x+0)=0），則解調的進行將更簡單，因為它將永遠用在右邊的表示式置換在左邊的表示式。一