007~9章 邏輯代理人、一階邏輯、一階邏輯中的推理

Post date: 2012/9/1 下午 12:49:14

七章 邏輯代理人

知識型代理人

知識為本代理人的核心部分是其知識庫,或稱KB(Knowledge Base)。

一個知識型代理人能夠僅要告訴他需要知道哪些事情而建構起來。以一個空的知識庫開始,代理人的設計者能一個語句一個語句的TELL該代理人,直到代理人知道如何在她的環境中運作為止。

wumpus世界

4*4格

4 stench NULL Breeze PIT

3 wumpus Gold PIT Breeze

2 stench NULL Breeze NULL

1 Start Breeze PIT Breeze

1 2 3 4

在洞穴的某處隱藏著一隻wumpus,一種惡獸,他會吃掉進入他房間的任何人。

代理人可以射殺wumpus,但是代理人只有一支箭。某些房間內有無底的陷阱,

遊戲目標是取得黃金。

效能指標:

撿到金子得+1000,掉入陷阱或者被wumpus吞噬得-1000,每採用一個行動-1,而用掉箭得-10。

代理人死掉或者代理人爬出山洞的時候比賽就算結束。

環境:

4*4的房間網格。代理人每次都從編號為 1,1 的方格出發,面向右方。

金子和wumpus的位置案均勻分配隨機除了起始方格以外的方格。另外,除了起始方格以外的任一方格都可能是一個陷阱,概率為0.2。

執行器:

代理人能向前走、TurnLeft(左轉)90度或TurnRight(右轉)90度。若他進入一個有陷阱或活著的wumpus的方格,

他將悲慘的死去。(進入一個有死wumpus的方格,是安全的,儘管很臭)。如果一個代理人試著向前移動而撞到一面牆壁,

那麼代理人部會移動。行動Grab可以用於撿起代理人所處方格內的一個物體。行動Shoot可以用於向代理人所正對的方向射出一支箭。

在沒有擊中wumpus(如果擊中,wumpus將被殺死)或者擊中牆之前,箭繼續向前運動。

代理人只有一支箭,因此只有第一個Shoot行動有效。最後,行動Climb(攀登)能用來爬出洞,但是只有方格 1,1。

感測器:

代理人具有5個感測器,每個都可以提供一些單一資訊:

─在wumpus所在之處以及與之直接相鄰(非對角的)的方格內,代理人可以感知到臭氣。

─在與陷阱直接相鄰的方格內,代理人感知到微風。

─在金子所處的方格內,代理人感知到閃閃金光。

─當代理人撞到牆時,他感知到撞擊。

─當wumpus被殺死時,他發出洞穴內任何地方都可感知到的悲慘嚎叫。

以5個符號的列表形式將感知資訊提供給代理人程式;例如,如果有臭氣和微風,但是沒有金光、撞擊或嚎叫,那麼代理人程式將接收到[ Stench,Breeze,None,None,None]。

邏輯

一個邏輯也一定要定義語意(semantics)或語句意義。語意定義了關於每個可能世界的每個語句其真值。

命題邏輯:一種非常簡單的邏輯

我們將論及命題邏輯的語法和他的語意確定語句真值的方式。

語法

命題邏輯的語法(syntax)係定義允許的語句。原子語句由單一個命題符號所組成。

語意

語意定義了用於判定關於特定模型的語句真值的規則。

一個簡單的知識庫

為wumpus世界構造一個知識庫。

為每個[x,y]位置我們需要下列符號:

如果在[x,y]有一個陷阱,則Px,y為真。

如果在[x,y]有一個死的或活的wumpus,則Wx,y為真。

如果代理人在[x,y]感覺有微風,則Bx,y為真。

如果代理人在[x,y]感覺到有臭氣,則Sx,y為真。

我們寫的句子將足以推倒 ┐P1,2(在[1,2]沒有陷阱)

我們將每個語句標示為Ri便於我們參用他們:

  • [1,1]中沒有陷阱:

R1: ┐P1,1

  • 一個方格裡有微風,若且唯若在某個相鄰方格中有陷阱。對於每個方格都必須說明這一情況;

目前,我們只包括了相關的方格:

R2: B1,1 ←→(P1,2 聯集 P2,1)

R3: B2,1 ←→(P1,1 聯集 P2,2 聯集 P3,1)

(a)

1,4 2,4 3,4 4,4

1,3 2,3 3,3 4,3

1,2 ok 2,2 3,2 4,2

1,1 A ok 2,1 ok 3,1 4,1

(b)

1,4 2,4 3,4 4,4

1,3 2,3 3,3 4,3

1,2 ok 2,2 P? 3,2 4,2

1,1 v ok 2,1 A B ok 3,1 P? 4,1

  • 在所有的wumpus世界中,前面的這些語句都為真。現在我們將代理人所處的特定世界中最初存取的兩個方格的微風感知資訊包括近來,

導出(b)中的場景。

R4: ┐B1,1

R5: B2,1

一個簡單的推理程式

我們第一個用來推論的演算法是一種直接運用蘊涵定義的模型檢查法:列舉出模型,

驗證a在KB為真的每個模型中為真。

命題定理之證明

我們蘊涵先給出一些與蘊涵相關的附加概念。

第一個概念是邏輯等價:兩語句a和b是邏輯等價的,如果他們在同一模型集合中為真。

我們將它寫成a=b 若且唯若 a|=b 且 b|=a

第二個概念是有效性。一個語句是有效的,如果在所有模型中她都為真。例如,語句P聯集┐P為有效的。有效語句也稱為恆真句─他們必為真。

對於任意語句a和b,a|=b若且唯若語句(a→b)是有效的

最後的概念是可滿足性。一個語句是可滿足,如果他於某些模型為真,或被某些模型所滿足。例如,先前給出的知識庫(R1聯集R2聯集R3聯集R4聯集R5)是可滿足的,

因為存在3個使他為真的模型,可透過列舉可能的模型直到發現某個滿足該語句的模型,而藉此檢驗可滿足性。

推理和證據

推倒一個證明的推理規則─引領至期望目標的結論鏈。

Modus ponens(斷言模式的拉丁話)

a→b, a

──────

b

此符號的意思是,只要給定任何形式為a→b的語句和a,就可以推導出語句b。

解消證明

我們論證了迄今為止所涉及的推理規則都是可靠的,但是我們還沒有對使用他們的推理演算法的完備性問題進行討論。

搜尋演算法,諸如迭代深入搜尋是完備的,在這個意義上,

他們可找到任何可到達的目標,但如果現有的推理規則是不適合的,那麼該目標是不可達的─沒有指使用那些推理規則之證明存在。

解消(resolution),當他和任何一個完備的搜尋演算法相結合時,可以得到一個完備的推理演算法。

解消規則只適用於文字的選言,因此他看來只和知識庫以及這樣的選言組成的查詢有關。

連言標準形

命題邏輯的每個語句邏輯等價於文字選言的連言。以子句的連言形式表示的語句被稱為連言標準形(conjunctive normal forn)或者CNF。

解消演算法

解消型推理法之運作是使用了稍前所介紹的矛盾證明原理。

命題邏輯的一個簡單解消演算法。函數PL-RESOLVE回傳對其兩個輸入作解消而得的所有可能子句的集合。

解消的完備性

如果子句集是不可滿足的,那麼這些子句的解消閉包包涵空子句。

霍恩子句和確定子句

一種如是限制的形式是確定子句,他是一個只有一個正文字的文字選言。

共通用些的是霍恩子句,其為至多只有一個正文字的文字選言。

前向和逆向連結

前向連結演算法PL-FC-ENTAILS?(KB,q)判定單個命題符號q─查詢─是否被霍恩子句的資料庫所蘊涵。

他從知識庫中的以知識時(正文字)開始。如果蘊涵的所有前提已知,那麼把他的結論添加到以知事實集。

例如,我在房子裡聽到開始下雨,我可能會想到野餐將取消。但是,我很可能部會想到我鄰居的花園裡最大的玫瑰的第17瓣花瓣將被淋濕;

人們把前向連結至於謹慎的控制之下,以免被無關結果淹沒。

逆向連結演算法,從該查詢逆向進行。

有效的命題模型檢驗

討論基於回溯搜尋,基於局部爬山法搜尋。這些演算法屬於命題邏輯「技術」的部分。

一個完備的回溯搜尋

及早終止

純符號啟發式

單元子句啟發式

元件分析

變數與值的排序

聰明後向跳躍演算法

隨機重新開始搜尋

聰明的索引

局部搜尋演算法

WALKSAT 簡潔有效的演算法之一。

演算法在每次迭代中選擇一個未得到滿足的子句並從該子句中選擇一個符號對其進行翻轉操作。

他在兩種方法中隨機選擇一個來挑選要翻轉的符號:

(1)最小衝突步驟,最小化新狀態下未滿足語句的數量,以及

(2)隨機行走步驟,隨機挑選符號。

隨機SAT問題的風貌

SAT問題比其他問題更難。容易的問題能被任何舊的演算法所解出,但是因為我們知道SAT是NP-complete,至少某些問題的實例需要指數級的執行時間。

命題邏輯型代理人

世界的當前狀態

知識庫由定理─對世界如何運作的一般性認識─與從代理人對特別世界經驗所獲得的認知與句。

推理wumpus世界之當前狀態的問題─我在哪兒,那個方格安全嗎。

那些與世界的持久不變知面向有關的符號並不需要時間上飆,有時也被稱為時間變數。

我們需要以一組邏輯語句寫下wumpus世界的轉移模型。

為了要描述世界是如何的改變,我們能試著寫出效應公理,該公理會敘明下於一個單位時間採取知行動會發生什麼事。

效應公理無法說出在行動之後有那些事物是保持原狀的。這件事的需要遂引起了框架問題。

框架問題的一個可能解決方法是加入可明確地斷言所有仍保持原狀之命題的框架公理。

框架公理之集合的規模是 O(mn)。 這個框架問題的特定表現有時被稱為表示框架問題。

對我們人類幸運地是,每個行動常常只改變那些流中少部分k個─世界展現局部性。

推理框架問題:於時間O(kt)而非O(nt)向前預測一個t單位時間之行動計劃之結果的問題。

代理人可能會被絆倒、心臟病發,被大蝙蝠帶走等等。敘明這些例外稱之限制問題(qualification problem)。

混合代理人

具有推論世界各方面之狀態的能力,可以相當直截了當地以條件─行動規則組合再一起,

並且配合第3章和第4章的問題求解問題演算法來為wumpus世界產生混合代理人。

邏輯狀態之估計

一個wumpus世界的混合代理人程式。他使用命題知識庫推理出世界的狀態,並使用問題求解搜尋和特定領域碼的組合來決定該採取什麼行動

上敘的代理程式運作得很好,但他有一個很大的弱點:隨著時間的逝去,呼叫ASK的計算費用變得越來越高。

我們不能有個代理人其處理每一個認知所需的時間是等比例於其生命的長度!我們真正需要的是固定不變的更新時間─也就是與 t 無關。

明顯的答案是儲存、或快取推理的結果,所以在下個單位時間的推理程序能建立在前一個時間所得到的結果,而非在一次從頭開始。

由命題推理的方式來訂定計畫

前面wumpus世界的混合代理人使用邏輯推理來判斷哪一個方格是安全的,但是使用A* 搜尋來訂定計畫。

這一節中,我們顯示該如何由邏輯推理訂定計畫。

1. 建構一條語句,其中包括

(a) Init ^0,一群有關切使狀態的斷言;

(b) Transition ^1,...,Transition ^t,後繼狀態公理用於每段時間內所有可能的行動直到最大時間t;

(c) 目標在時間 t 達成的斷言;HaveGold ^t ^ ClimbedOut ^t。

2. 將整個語句呈現予一個SAT求解程式。如果求解程式找出一個滿意的模型,那麼目標是可達成的;如果該語句是無法滿足的,那麼訂定計畫的問題是不可能的。

3. 假定某個模型被找出,從那些代表行動且被賦予為真的變數中抽取出來。兜起他們就代表了達成該目標的計畫。

我們已經介紹了知識型代理人,並且說明了如何定義一種邏輯,使得代理人可以對世界進行推理。要點如下:

  • 智慧型代理人需要關於世界的知識,以便達到良好的決策。
  • 知識是利用語句形式被包含在代理人內,這些語句是採知識表示語言,並儲存在知識庫中。
  • 知識型代理人是由知識庫和推理機制組成的。他的運轉方式是把關於世界的語句儲存到他的知識庫中,運用推理機制推導出新的語句,並用這些語句來決策採取什麼行動。
  • 表示語言是透過他的語法和語意來定義,其中語法指定語句的結構,而語意定義了每個語句在每個可能世界或模型中的真值。
  • 語句之間的蘊涵關係對於我們對推理的理解至關緊要。語句a蘊涵另一語句b,如果b在所有a為真的世界中都為真。等價定義包括語句a=>b的有效性和語句a^ ┐ b的不可滿足性。
  • 推理是從舊語句中產生新語句的過程。可靠推理演算法只產生被蘊涵的語句;完備演算法產生所有被蘊涵的語句。
  • 命題邏輯是由命題符號和邏輯連結符組成的簡單語言。他可以處理已知為真、已知為假或完全未知的命題。
  • 已知一個固定的命題詞彙表時,可能模型集是有限的,因此蘊涵檢驗可以透過對模型進行列舉來實作。用於命題邏輯的有效模型檢驗推理演算法包括回溯和局部搜尋方法,通常可以快速求解大規模的問題。
  • 推理規則是可用來尋找證明的可靠推理模式。解消規則產生一個用於已連言標準型表示的知識庫之完備推理演算法。前向連結和逆向連結是用於以霍恩形式表示的知識庫之自然推理演算法。
  • 局部搜尋演算法像是WALKSAT能被使用來找出解答。這樣的演算法是不錯但是不完備。
  • 邏輯狀態估算涉及維持一個邏輯語句,此語句描述出與觀察歷史一致的可能狀態集合。每個更新步驟需要使用該環境的轉移模型來推理,這是建構在敘明每個流是如何改變的後繼狀態公理。
  • 一個邏輯代理人之間的決定能被SAT解出:找出的可能的模型,於此敘明到達目標之未來的行動順序。這種方式只對完全可觀察或無感測的環境有效。
  • 命題邏輯部會配合範圍限制之環境來調整,因為他缺乏簡潔處理時間、空間和物件之間的一般性關係樣式的表達力。

八章 一階邏輯

表示法的回顧

我們將著眼於命題邏輯和其他類型的語言以便瞭解這些語言能做什麼不能做什麼。

程式語言(例如C++、JAVA或LISP)是到目前為止常用的形式語言中最大的一類。

想法的語言

自然語言確是富於表達力的。我們設法幾乎全部用自然語言來寫作這整本書

「本節中,我們將討論表示語言的本質‧‧‧」

「本節涵蓋了知識表示語言的主題‧‧‧」

攀登最佳的形式與自然語言

我們的法方將要採用命題邏輯的基礎───即一種陳敘式、上下文無關且不含糊的合成語意───並在這一基礎上,借用自然語言的表達想法,同時避開它的缺點,並在此基礎上構造出一種更具表達能力的邏輯。

一階邏輯的語法和語意

一階邏輯的模型

首先,他們內部包含有物件!一個模型的領域(domain)是它所包含的物件或者領域元件的集合。領域必須是非空的─每個可能的世界一定要至少包含一個物件。

符號和解釋

我們現在轉向一階邏輯的語法。

Sentence → AtomicSentence | ComplerSentence

AtomicSentence → Predicate | Predicate(Term,...) | Term = Term

ComplerSentence → (Sentence) | [ Sentence ]

| ┐ Sentence

| Sentence ^ Sentence

| Sentence ˇ Sentence

| Sentence → Sentence

| Sentence ←→ Sentence

| Quantifier Variable,... Sentence

Term → Function(Term,...)

| Constant

| Variable

Quantifier → 倒A | 倒E

Constant → A | X1 | John | ....

variable → a | x | s | ...

Predicate → True | False | After | Loves | Raining | ...

Function → Mother | LeftLeg | ...

OPERATOR PRECEDENCE : ┐,=^ˇ,→,←→

一階邏輯的等式語法,以Backus-Naur形式來表現。運算元的優先次序已敘明,從最高到最低。量詞的優先次序是使得量詞對其又任何符號成立

一個項是一個物件的一個邏輯運算式

原子語句

我們已經有了指到物件的項即指到關係的述詞符號。我們可以把他們放在一起形成陳述事實的原子語句。

複雜語句

搭配同命題演算中的語法及語義,我們可以用邏輯連接符來建構更複雜的語句。

量詞

一旦我們有了允許物件存在的邏輯,那麼很自然地我們想要表達全部物件集合的屬性,而不是根據名稱列舉物件。

全稱量詞(倒A)

全稱量詞對每一個物件進行陳述。

x→獅心王理查

x→約翰王

x→理查的左腿

x→約翰的左腿

x→王冠

如果語句King(x) → Person(x)在5種擴展解釋下都為真,那麼在原始解釋模型中,全稱量化語句倒Ax King(x) →Person(x)即為真。

也就是說,全稱量化語句等價於斷言下列5個語句:

獅心王理查是國王→獅心王理查是人

約翰王是國王→約翰王是人

理查的左腿是國王→理查的左腿是人

約翰的左腿是國王→約翰的左腿是人

王冠是國王→王冠是人

存在量詞(倒E)

我們可以對全域中的某個物件進行陳述而無須對它命名,透過使用存在量詞。

倒Ex Crown(x) ^ OnHead(x,John)

倒Ex讀為「存在一個x,這樣以至......」或「對於某個x.....」。

語句倒Ex P表示至少對於一個物件x,P為真。

獅心王理查是王冠 ^ 獅心王理查在約翰的頭上

約翰王是王冠 ^ 約翰王在約翰的頭上

理查的左腿是王冠 ^ 理查的左腿在約翰的頭上

約翰的左腿是王冠 ^ 約翰的左腿在約翰的頭上

王冠是王冠 ^ 王冠在約翰的頭上

第 5 條斷言在模型中為真,因此原先的存在量化語句在模型中為真。

需要注意的是,根據我們的定義,該語句在約翰王帶著兩個王冠的模型中可能也為真。

巢狀量詞

我們通常希望採用多個量詞來表示更複雜的語句。

最簡單的情況是具有相同類型的量詞。

例如,「兄弟是同胞」可表示為:

倒x倒y Brother(x,y)→Sibling(x,y)

同類型的多個連貫的量詞可以寫成一個具個數個變數的量詞。

「每一個人都會喜愛某人」的意思為,對於每一個人,都會存在此人喜愛的某人:

倒Ax 倒Ey Loves(x,y)

要說「存在一個被每一個人都喜愛的人」,我們寫為:

倒Ey倒Ax Loves(x,y)

因此,量詞的順序很重要。

倒A與倒E之間的連接符

這兩個量詞透過「非」操作實際上緊密相關。斷言每個人都不喜歡歐洲防風草等同於斷言不存在某個喜歡歐洲防風草的人;反之亦然:

倒x ┐Likes(x,Parsnips) 等價於 ┐倒Ex Likes(x,Parsnips)

我們可以更進一步:「每個人都喜歡茄子」意味著沒有一個人不喜歡茄子:

倒Ax Likes(x,eggplant) 等價於 ┐倒Ex ┐Likes(x,eggplant)

等式

我們能使用平等符號象徵兩個期限提及相同的物件。例如,

Father(John) = Henry 約翰的父親 = 亨利

表示Father(John)指代的物件和Henry所指代的物件是相同的。

替代語句?

「理查的兄弟是約翰和傑佛瑞」

Brother(John,Richard) ^ Brother(Geoffrey,Richard) ^ Joh =/= Geoffrey ^ 倒Ax Brother(x,Richard) →(x = John ˇ x = Geoffrey)

一個非常流行於資料庫系統的建議做法如下。首先,我們堅持每一個常數符號必須參照到一個具體的物件─稱之為名稱唯一假設(unique-names assumption)。

其次,我們假定不知道為真之原子語句都視之為假─封閉世界假設

最後,我們援用領域封閉性,意味著每個模型包含的領域元件個數不會多於被常數符號所命名者。

於此產生的語義,我們稱之為資料庫語義,以便將他與一階邏輯的標準語義區別開來

使用一階邏輯

一階邏輯中的斷言和查詢

與命題邏輯完全一樣,用TELL將語句添加到知識庫中。這樣的語句被稱為斷言。

例如,我們可以斷言約翰是國王,理查是一個人,且所有國王都是人:

TELL(KB,King(John))

TELL(KB,Person(Richard))

TELL(KB,倒Ax King(x)→Person(x))

我們可以用ASK像知識庫詢問問題。例如,

ASK(KB,King(John))

回傳true。用ASK提問的問題稱為查詢或目標。

親屬關係領域

我們考慮的第一個實例是關於家庭關係或稱親屬關係的領域。

數字、集合和列表

數字可能是如何從微小的公理核心建立起一個大型理論的最生動實例。我們將在此描述自然數或非負整數的理論。

一旦我們有了加法,就可以直接把乘法定義為反覆的加法、求冪定義為反覆的自乘、整數除法和餘數、質數等等。

列表(lists)與集合非常相似。他們的差別在於列表是有順序的,而且同一個元素可以在一個列表中出現不只一次。

wumpus 世界

本節介紹的一階邏輯公里相對而言更加簡明,以一種非常自然的方式捕捉到我們希望表訴的內容。

一階邏輯的知識工程

知識工程師對特定領域進行調查,總結出在該領域的重要概念,建立該領域內的物件和關係的形式表示。

知識工程的過程

1. 確定任務

知識工程師必須勾畫出知識庫支持的問題範圍以及˙對每個特定的問題實例可以採用那些種類的事實。

2. 蒐集相關知識

知識工程師可能已經是該領域的專家,或者還需要和真正的專家進行合作以便提取專家的知識─這一過程被稱為知識獲取。

3. 確定述詞、函數和常數的詞彙表

也就是把重要的領域級概念轉換為邏輯級的名稱。

4. 對領域的通用知識進行編碼

知識工程師對所有詞彙項寫出公理。

5. 將對特定問題實例的描述進行編碼

他涉及寫出已經是本體論的一部份的概念實力的簡單原子語句。

6. 把查詢提交給推理過程並獲取答案

我們可以讓推理過程對公理和特定問題的事實進行操作,從而推導出我們有興趣了解的內容。

7. 除錯知識庫

他可以透過注意推理鏈意外停止之處來確定缺失或者過弱的公理。

電路領域

確定任務

蒐集相關知識

選定詞彙表

對領域的通用知識進行編碼

對特定問題的實例進行編碼

把查詢提交給推理過程

除錯知識庫

本章介紹了一階邏輯,一種比命題邏輯表達能力更強的表示語言。要點如下:

  • 知識表示語言應該是陳述性的、可合成的、有表達能力的、上下文無關的以及無歧異的。
  • 邏輯學在他們的本體論約定和知識論約定上存在不同。命題邏輯只是對事實的存在進行限定,而一階邏輯對於物件和關係的存在進行限定,因而獲得更強的表達能力。
  • 一階邏輯的語法建立於命題邏輯之上。他增加術語來代表物件,而且有全稱性和存在性的量詞來建構全部或某些被量化之變數的可能值。
  • 一階邏輯的可能是借,或模型,包括一組物件和解釋,解釋會把常數符號映射到物件,把述詞符號映射到物件之間的關係,及函數符號映射到物件的功能。
  • 只有當透過述詞命名的關係再透過項命名的物件之間成立的時候,原子語句才為真。擴展解釋,他把量詞變數映射到模型中的物件,定義了量詞的真假值。
  • 在一階邏輯中開發知識庫是一個細緻的過程,包括對領域進行分析、選擇詞彙表、對支持所需推理必不可少的公理進行編碼。

九章 一階邏輯中的推理

本章中我們將定義供回答以一階邏輯形式提出的問題的有效過程。

命題與一階推理

量詞的推理規則

我們首先從全稱量詞開始。假定我們的資料庫包含了標準的民間傳說公理,他認定所有貪婪的國王都是邪惡的:

倒x King(x) ^ Greedy(x) →Evil(x)

全稱實例化(universal instantiation,簡寫為UI)

對於存在實例化之規則,該變數被單一新的常數符號所取代。

簡化成命題推理

一旦我們有了從量化語句推理非量化語句的規則,就可以將一階推理簡化為命題推理。

統一和提升

一階推理規則

「約翰是邪惡的」之推理─亦即,{x | John}解出查詢 Evil(x)─的方式如下:

欲使用規則「貪婪的國王是邪惡的」找出某些 x 使得 x 是國王且 x 是貪婪的,然後推論出 x 是邪惡的。

更一般地,如果有某個互換 系她 使蘊涵的前提和知識庫中已有的語句完全相同,那麼應用 系她 後,我們就可以斷言蘊涵的結論。

在本實例中,互換 { x | John} 就達到了這個目的。

統一

被提升的推理規則要求找到相關的互換,讓不同的邏輯表示看起來是一樣的。這個過程稱為統一,且是所有一階推理演算法的一個關鍵部分。

統一演算法 UNIFY 挑選兩條語句並返回一個他們的統一者(unifier),如果存在的話:

UNIFY(p,q)= 系她 ,這裡SUBST(系她,p) = SUBST(系她,q)

對統一的兩個語句中的一個進行標準化分離就可以避免該問題,也就是對這些變數重新命名以避免名稱衝突。

對每個運算式的統一對,存在一個唯一的最一般統一者(或稱MGU)

儲存和檢索

用來通知和詢問知識庫的TELL和ASK函數的下層是更原始的STORE和FETCH函數。STORE(s)將語句儲存到知識庫中,

FETCH(q)返回所有統一者,這些統一者能使查詢q與知識庫中的某些語句統一。

我們用於說明統一的問題─找出所有與Knows(John,x)統一的事實─就是FETCHing的一個實例。

實作STORE與FETCH的最簡單方法是保存所有的事實於一個長長的清單並且統一各個查詢與該清單上的每個元素。

前向連結

一階確定子句

一階確定子句非常雷同於命題確定子句:他們是文字的選言,其中恰好只有一個是正文字。

確定子句可以是原子語句,或者是蘊涵語句,它的前提為正文字的連言,結論是一個單獨的正文字。

「......美國人賣武器給敵對國家是犯法的」:

American(x) ^ Weapon(y) ^ Sells(x,y,z) ^ Hostile(z) → Criminal(x)

一個簡單的前向連結演算法

function FOL-FC-ask(KB,a) return a substitution or false

inputs: KB, the knowledge base, a set of first-order definite clauses

a,the query, an atomic sentence

local variables: new, the new sentences inferred on each iteration

repeat until new is empty

new ← {}

for each rule in KB do

(p1 ^ ... ^ pn →q) ← STANDARDIZE-VARIABLES(rule)

for each 系她 such that SUBST(系她,p1 ^ ... ^ pn) = SUBST(系她,p'1 ^ ... ^ p'n)

for some p'1,...,p'n in KB

q' ← SUBST(系她,q)

if q' does not unify with some sentence already in KB or new then

add q' to new

中←UNIFY(q',a)

if 中 is not fail then return 中

add new to KB

return false

一個概念上簡明直接、但效率非常低的前向連結演算法。在每次疊代過程中,演算法把所有只用一步就可以從KB中已有的蘊含語句和原子語句推倒出來的原子語句都添加到KB中。函數STANDARDIZE-VARIABLES以先前未曾使用過的新變數來替換於他參數中的所有變數

有效率的前向連結

演算法中有3種可能的無效率來源。

第一,演算法內的「內迴圈」涉及尋找所有可能的統一性,把規則的前提與知識庫中一個適合的事實集進行統一。

這一過程通常被稱為模式匹配(pattern matching),他的成本可能很高。

第二,演算法每次尋訪都要對每條規則進行重新檢查,以觀察其前提是否已經得以滿足,即使每次尋訪添加到知識庫的規則非常少,也要全部檢查。

最後,演算法可能產生許多與目標無關的事實。

將規則匹配於已知事實

把規則前提與知識庫中的事實進行匹配的問題可能看起來足夠簡單。

例如,假設打算使用規則

Missile(x) → Weapon(x)

那麼我們需要找出所有能與Missile(x)統一的事實;在已經建立了是當索引的知識庫中,這一過程對於每個事實都可以在常數時間內完成。

連言項排序問題:尋找一個順序來解決規則前提的連言項,以使得總成本最小。

增量前向連結

當我們說明前向連結在犯罪例子中如何工作時,我們使了詐;特別是,我們省略了由一個簡單的前向連結演算法所示的演算法完成的某些規則匹配。

無關的事實

前向連結中最後一個無效率的來源似乎是這一方法所固有的,同時他也會在命題文脈出現。

反向連結

逆向連結演算法

圖9.6

一階知識庫所用的簡單逆向連結演算法

顯示確定子句所用的一個逆向連結演算法。

FOL-BC-ASK(KB, goal)會被證明如果知識庫包含一個 lhs → goal 形式的子句,其中 lhs(左手側) 是一個連言項列表。

邏輯程式設計

邏輯程式設計是相當接近於第七章中描述的陳述性想法的一種技術:應該採用正規語言表達知識從而建構系統,並且應該在這些知識上執行推理過程從而求解問題。

該想法可以用羅伯特‧科瓦爾斯基(Robert Kowalski)的等式進行總結,

演算法 = 邏輯 + 控制

Prolog 是最廣泛的邏輯程式語言。

有效率的實作邏輯程式

Prolog 程式的執行有兩種模式:解釋執行和編譯執行。解釋本質上相當於將程式當作知識庫來執行圖9.6的FOL-BC-ASK演算法。我們說「本質上」,因為Prolog解釋器包含各種為了最大化速度而設計的改進方法。我們在此只考慮其中的兩種。

多餘的推理與無限的迴路

現在我們轉向Prolog的阿基里斯之踵(唯一致命弱點):深度優先搜尋與包含了重複狀態和無線路徑的搜尋樹之間的不匹配。

Prolog 的資料庫語意

唯一名稱假設說Prolog的每一個常數以及每一個基項集參照到一個獨一無二的物件,而封閉世界假設說僅有那些為知識庫所蘊含者的語句才為真。

限制邏輯程式設計

在我們對前向連結的討論中,我們顯示了限制滿足問題(CSP)如何被編碼程確定子句。

標準的Prolog用悍圖6.5給出的回溯演算法完全一樣的方法求解這類問題。

解消

一階邏輯的連言標準型

如同在命題邏輯中,一階邏輯的解消也要求語句必須是連言標準型(CNF)─即子句的連言,其中每個子句是文字的選言。文字可以包含變數,假設這些變數是全稱量化的。

例如,語句

倒x American(x) ^ Weapon(y) ^ Sells(x,y,z) ^ Hostile(z) → Criminal(x)

以CNF表示,變成

倒x American(x) ^ Weapon(y) ^ Sells(x,y,z) ^ Hostile(z) → Criminal(x)

一階邏輯的每個語句都可以轉換成一個推理等架的CNF語句。特別是,CNF語句只有當原始語句不可滿足時才不可滿足,因此我們證明的基礎是CNF語句上的反證法。

解消推理規則

一階邏輯子句的解消規則只是 7.5.2節所給的命題解消規則的提升版本。

假設兩個子句已經標準化分離,因此他們沒有共用變數,那麼如果包含互補文字,則他們是可解消的。如果一個命題文字是另一個命題文字的否方式,則這兩個命題文字是互補的;

如果一個一階邏輯文字能和另一個一階邏輯文字的否方式合一,則這兩個一階邏輯文字是互補的。

這是藉由以統一者 系她 = {u/G(x), v/x} 消除互補文字 Loves(G(x),x) 和 ┐ Loves(u,v),然後產生解消子句:

這個規則稱之為二元解消規則,因為他剛好解消了個文字。

證明範例

藉由證明 KB |= ┐ a 是不可滿足的,也就是說,藉由推倒該空子句來解消證明 KB ^ ┐ a。這個演算法所採用的方法和如圖7.12所描述的命題邏輯的情況是完全一樣

第一個是來自第9.3節的犯罪例子。CNF語句為

我們把否定目標┐Criminal(west)也包含在CNF語句中。

第二個實例利用了Skolem化並涉及非確定子句。這就造成了一個多少有點複雜的證明結構。用英語來表示,該問題可以表示成:

愛所有動物的人被某個人愛著。

任何殺了動物的人沒有人愛。

Jack 愛所有的動物。

Jack 和 Curisoity 其中的一個人殺死了那只名叫 Tuna 的貓。

是 Curiosity 殺害了那只貓嗎?

首先,我們將這些原始語句、某些背景知識和目標G的否定用一階邏輯形式表達:

現在我們利用轉換過程將每個語句轉換成CNF:

Curiosity 殺了那只貓的解消證明如圖9.12所示。在自然語言中,證明可以譯義成:

設Curiosity沒有殺害Tuna。我們知道不是Jack就是Curiosity做的;因此一定是Jack幹的。

現在,Tuna是一隻貓,而貓是動物,所以Tuna是一隻動物。因為殺了動物的任何人沒有

人愛,那麼我們知道沒有人愛Jack。另一方面,Jack喜愛所有的動物,因此一定有某人愛

他;如此,就出現了矛盾。所以,是Curiosity殺害了那只貓。

解消的完備性

此節將證明解消為反證法完備,這意味著如果一個語句集不可滿足,那麼解消總會導出一個矛盾。

等式

本節目前所描述過的推理的方法中,沒有一個是處理 x = y 形式的斷言。

有三個具體的方法可資採用。

第一種、等式公理化─寫下與知識庫中等是關係有關的語句。

第二種、 解調法(demodulation)

調解法(paramodulation)

第三種、完全在擴展的統一演算法裡處理等式推理。

解消策略

單元優先:優先對那些包含一個單文字(也就是單元子句)的語句進行解消。

支撐集:首先嘗試某些解消的優先策略對於解決問題很有幫助,但是一般來說試圖減少一些潛在的解消要更有效。

輸入解消:在輸入解消策略中,每個解消把一個輸入語句(來自KB或者查詢)和某個其他語句結合起來。

包容法:清除所有被知識庫中的已有語句包容(即,比該語句更加特定)的語句。

定理證明機的實際應用

理論證明機可以運用於與軟體與硬體的合成與驗證有關之問題。

我們已經對一階邏輯中的邏輯推理以及實作推理的許多演算法進行了分析。

  • 第一個方式使用推理規則(全稱實例化與存在實例化)來命題化推理問題。通常,這個方式很慢,除非領域很小。
  • 運用統一來便是合適的變數互換消除了一階證明時的實例化步驟,使得該過程在許多情況下更有效率。
  • 肯定前件(Modus Ponens)的一個提昇版本利用合一提供了一條自然而且強大的推理規則,一般化肯定前提。前向連結和逆向連結演算法把這條規則應用於確定子句的集合。
  • 儘管蘊涵問題是半可判定的,一般化肯定前提對於確定子句仍然是完備的。對於由不含函數的確定子句所組成的Datalog知識庫,蘊涵是可判定的。
  • 前向連結用於演繹資料庫中,它可以和關聯資料庫的操作結合起來。前向連結還用於產生式系統中,對非常龐大的規則及進行高效率的更新。前向連結對於Datalog程式而言是完備的,而且其執行時間是多項式的。
  • 邏輯程式設計系統中採用了逆向連結,他還使用複雜的編譯技術保證了非常快速的推理。逆向連結需要承受冗餘推理和無限迴圈;這些問題可以在一定程度上透過備忘法緩解。
  • Prolog,不像一階邏輯,使用一個封閉的世界具有唯一名稱假設,並且否定視為失敗。這些使得Prolog是一個更實用的程式語言,不過卻與純邏輯相去更遠。
  • 一般化解消推理規則為一階邏輯提供了一個完備的證明系統,該系統採用連言範例形式表示的知識庫。
  • 存在一些用於減少解消系統的搜尋空間而不影響其完備性的策略。最重要的問題之一是處理等式;我們會展示如何使用解調法與調解法。
  • 有效的基於解消的定理證明機已經被用於證明受關注的數學定理以及用來對軟體和硬體進行驗證和合成。