本文關(guān)鍵詞：歸納邏輯程序設(shè)計初探，由筆耕文化傳播整理發(fā)布。

了，而消解的主要原理來自于羅賓遜（J.A.Rob；2.2.2赫爾布蘭德解釋；前面我們說明了，為了證明A→B，只需證明經(jīng)過反證；下面我們就介紹一個這樣的論域，，即赫爾布蘭德域；定義2.12集合H稱為子句集S的赫爾布蘭德域，如；H0=；{c∣c為S中出現(xiàn)的常元}；H1=H0∪{f（t1，t2，?，tn）∣t1，；因為子句集中沒有常元，因此H0={a}；H1={a,

了，而消解的主要原理來自于羅賓遜（J.A.Robinson）在1965年提出的消解原理，這個原理是羅賓遜在赫爾布蘭德（Herbrand）理論的基礎(chǔ)上產(chǎn)生的。那么我們就先來了解一下赫爾布蘭德理論中的核心概念——赫爾布蘭德解釋。

2.2.2 赫爾布蘭德解釋

前面我們說明了，為了證明A→B，只需證明經(jīng)過反證法變換的一階公式A∧?B是不可滿足的即可。所謂不可滿足就是指對于所有論域上所有可能的解釋，A∧?B均取假值。而一階邏輯公式的解釋往往有無窮多種，研究所有論域上的所有解釋是不方便的，也是不可能的。如果可以把一階邏輯公式的子句集在任意域上的不可滿足問題轉(zhuǎn)化在一個比較簡單的特殊論域上的不可滿足問題。那么這個問題就簡單很多。

下面我們就介紹一個這樣的論域，即赫爾布蘭德域。

∞

定義2.12 集合H稱為子句集S的赫爾布蘭德域，如果H= ∪ Hi，其中Hi遞歸定義如下： i = 0 {a} 當(dāng)S中無任何常元出現(xiàn)時，H0由任意單個常元構(gòu)成，如{a}，

H0=

{c∣c為S中出現(xiàn)的常元}

H1= H0∪{f（t1，t2，?，tn）∣t1，t2，?，tn ∈H0，f為S中出現(xiàn)的函數(shù)符號} H i +1 = Hi∪{ f（t1，t2，?，tn）∣t1，t2，?，tn ∈Hi，f為S中出現(xiàn)的函數(shù)符號} 例如：設(shè)子句集S={P(x)∨?Q(x), R(f(x)), ?P(y) ∨?R(x)}，那么這個子句集的赫爾布蘭德域為：

因為子句集中沒有常元，因此H0={a}

H1={a, f(a)}

H2={a, f(a), f(f(a)) }

???

H∞={a, f(a), f(f(a)), f(f(f(a))), ? }

為了討論方便，我們需要以下術(shù)語：

定義2.13如果項、原子公式、文字、子句以及代入實例中沒有變元，那么它們分別稱為基項、基原子公式、基文字、基子句和基例。

根據(jù)這個定義，赫爾布蘭德域中的元素，事實上是一階語言中的一些基項。我們知道一階邏輯公式在不同的論域上可以有不同的解釋，那么在赫爾布蘭德域上對一階邏輯公式也要有解釋。有如下定義：

定義2.14子句集S在其赫爾布蘭德域H上的解釋稱為赫爾布蘭德解釋（用I（H）表示），

它滿足如下條件：

（1） 在I（H）下，常元映射到自身。

（2） 對S中的任一n元函數(shù)f，I（H）(f)為赫爾布蘭德域H上的函數(shù)，且對于t1,t2,?,tn

∈H，I（H）(f(t1,t2,?,tn))= f(t1,t2,?,tn)。

（3） 對S中的任一謂詞P，I（H）(P)是赫爾布蘭德域H上的關(guān)系。

赫爾布蘭德解釋是把一階語言中的基項解釋為基項自身，解釋之后這個被解釋的基項就是赫爾布蘭德域中的元素。這樣，子句集的不可滿足問題轉(zhuǎn)化為S在其赫爾布蘭德域上的不可滿足問題，有如下定理：

定理2.2子句集S是不可滿足的，當(dāng)且僅當(dāng)所有赫爾布蘭德解釋都不滿足S。

如果S中有個體常元，則它的赫爾布蘭德域是唯一的。

赫爾布蘭德還給出了赫爾布蘭德定理。這個定理在人工智能的發(fā)展中具有重要作用。因為本文重點討論在機(jī)器上實現(xiàn)機(jī)器定理證明的消解定理，因此此處不再贅述赫爾布蘭德定理，接下來我們重點介紹羅賓遜的消解定理。

2.2.3 消解原理

前面我們提到了，消解就是從子句中消去一些項的機(jī)械過程，目的是產(chǎn)生空子句，從一階邏輯公式的不可滿足性，證明待證定理。羅賓遜將消解定理定義如下：

定義2.11 令L1為一個正文字，L2為一個負(fù)文字，如果?L1=L2，則L1和L2形成一個互補(bǔ)對。

定理2.2（消解原理）： 設(shè)C1，C2是子句集中的任意兩個子句，如果C1中的文字L1與C2 中的文字L2形成一個互補(bǔ)對，則從C1和C2中分別消去L1和L2，并將這兩個子句中余下的部分做析取構(gòu)成一個新的子句C12，稱這一過程為消解，所得到的子句C12稱為C1和C2的消解式，稱C1和C2 為C12的親本子句。形式如下：

C1=A∨L1 ，C2=B∨L2

C12=A∨B

也可以表示為C12=（C1–{L1}）∪（C2– {L2}），這里“–”表示“集合差運算”。 根據(jù)消解定理，消解式C12是其親本子句C1和C2的邏輯結(jié)論。同時也可以得到一個推論，即把得到的消解式再放入子句集中，繼續(xù)進(jìn)行消解，直至得到空子句，從而程序停止，定理得到證明。

推論2.1 設(shè)C1和C2是子句集S中的子句，C12是C1和C2的消解式。如果把C12加入子句集S后得到新子句集S1，則S1和S是同可滿足性的，即：S是不可滿足的當(dāng)且僅當(dāng)S1是不可滿足的。

在消解的過程中，還有一個問題時必須要注意的，由于在子句中可能存在個體變元和函數(shù)，所以從子句集中尋找子句的互補(bǔ)對就比較復(fù)雜了，因此，需要對子句執(zhí)行一些操作，使得一階邏輯公式可以與計算機(jī)的模式相匹配，這些操作就是置換和合一。

置換（substitution）又名替換或代換。目的是在若干看起來個體變元完全不相同的子句中，通過置換的手段使不同子句變元表達(dá)符號一致，從而便于找到消解式，以便能進(jìn)行消解。置換可以簡單地理解為在一個子句中，用置換項替換個體變元，本質(zhì)上是變元到項的任意映射。正式的定義如下：

定義2.12 置換是形如{t1/x1，t2/x2，……，tn/xn}的一個有限集。其中，xi是變元，ti是項。不含任何元素的置換稱為空置換，用ε表示。

例：有下述若干命題：

（1）所有不富有并且聰明的人是快樂的。

（2）喜歡音樂的人是聰明的。

（3）Peter喜歡音樂并且不富有。

（4）快樂的人過著激動人心的生活。

求證：Peter過著激動人心的生活。

證明： 根據(jù)題干，給出謂詞

根據(jù)題意，可列出以下一階邏輯公式

可將條件和求證目標(biāo)放在一起，并化為子句形式，可得：

（1） Rich(x)∨?Smart(x)∨Happy(x)

（2）?Music(x)∨Smart(x)}

（3）Music(Peter)

（4）? Rich(Peter)

（5）?Happy(x)∨Exciting(x)

（6）?Exciting(Peter)

對上述子句消解處理：

（7）?Happy(Peter) （（5）、（6）作置換{ Peter /x}然后消解）

（8）Smart(Peter) （（2）、（3）作置換{ Peter /x}然后消解）

（9）? Smart Peter)∨Happy(Peter) （（1）、（4）作置換{ Peter /x}然后消解）

（10）? Smart(Peter) （（7）、（9）消解）

（11）Smart(Peter) ∧? Smart(Peter)? □ （（8）、（10）消解，得到空子句）

所以Peter過著激動人心的生活。

以上這個例子很好地揭示了置換和消解過程。所謂合一（unify）是指通過置換，使得不同的表達(dá)式變?yōu)橄嗤谋磉_(dá)式的算法。

定義2.13 設(shè)有表達(dá)式集{E1，E2，……，En}和置換θ，使E1θ=E2θ= …=Enθ，便稱E1，E2，……，En是可合一的，且θ稱為合一置換（不是唯一的）。5

例如：集合{P(x),P(f(y))}是可合一的，因為置換θ={f(a)/x, a/y}使得P(x)θ=P(f(a))= P(f(y))θ=P(f(a))。因此θ是合一置換。

定義2.14 若E1，E2，……，En有合一置換σ，且對E1，E2，……，En的任一合一置換θ，都存在一個置換λ，使得θ=σλ，則稱σ是E1，E2，……，En的最一般合一置換，記作mgu。

根據(jù)最一般合一置換，前面的消解式也可以表示為：

C12=（C1σ–{L1σ}）∪（C2σ– {L2σ}）

置換與合一的作用除了進(jìn)行模式匹配之外，還有簡化推理過程的作用，因為在機(jī)器定理證明過程中，推理中子句數(shù)量往往成指數(shù)級增長，包括產(chǎn)生的大量冗余的子句，降低了推理的效率，因此要刪除或減少這些冗余。

以上就是合一消解系統(tǒng)的基本內(nèi)容，它是機(jī)器定理證明的基礎(chǔ)，也是我們后面要討論的歸納邏輯程序設(shè)計的邏輯基礎(chǔ)。其消解的過程可以概述如下：

合一消解的過程6如下：

（1） 寫出一階邏輯公式；

（2） 將一階邏輯公式用反證法形式寫出；

（3） 將由（2）得到的公式轉(zhuǎn)化為合取得Skolem標(biāo)準(zhǔn)型；

（4） 求�。�3）的子句集S；

（5） 對S中可消解的子句做消解；

（6） 由（5）得到的消解式仍放入S中，重復(fù)消解過程；

（7） 得到空子句；

（8） 定理得證。

下面我們來介紹子句邏輯的另一個重要的系統(tǒng)，霍恩子句推理系統(tǒng)，這個系統(tǒng)是形成歸納邏輯程序設(shè)計基礎(chǔ)的重要系統(tǒng)。

2.3 霍恩子句推理系統(tǒng)

前面我們已經(jīng)看到，一階邏輯具有很強(qiáng)的表述能力，使得一階邏輯的消解定理在進(jìn)行機(jī)器定理證明、問題求解等方面發(fā)揮了重要的作用。為了使問題的描述更加簡明、自然，5

6 E是表達(dá)式，θ是置換，Eθ是對表達(dá)式E進(jìn)行置換θ后得到的結(jié)果。 馬少平 朱小燕/著 人工智能 清華大學(xué)出版社 2004年8月第一版，107頁

并具有一定的過程意味，需要使推理過程程式化，這就需要一個重要的工具，即霍恩子句，這個子句因邏輯學(xué)家A.霍恩（Horn）對其性質(zhì)作了詳盡的研究，故而得名。關(guān)于子句的定義前面已經(jīng)講過了，下面我們就定義什么是霍恩子句以及由此發(fā)展出的邏輯程序設(shè)計。

2.3.1 霍恩子句

前面我們定義了子句是若干文字的析取，因此子句C1=P1∨P2∨??∨Pm∨?Q1∨?Q2∨??∨?Qn可以表示為C2=Q1∧Q2∧??∧Qn→P1∨P2∨??∨Pm。如果我們可以約定這個蘊涵式的前件的文字間恒為合取，而后件的文字間恒為析取，那么可以將C2改寫為C3= Q1,Q2,?,Qn→P1,P2,?,Pm。這里我們由于技術(shù)上的原因，將這個C3改寫成為：

（1） C=P1,P2,?,Pm←Q1,Q2,?,Qn。其中“P1,P2,?,Pm”這部分稱為子句頭，

“Q1,Q2,?,Qn”稱為子句體。

當(dāng)m=0時，（1）可以寫成：

（2） C=←Q1,Q2,?,Qn。

當(dāng)n=0時，（1）可以寫成：

（3） C=P1,P2,??,Pm←。

這樣的子句蘊涵表達(dá)形式使得問題的描述更接近問題的自然描述，使得許多問題的形式表述可以直接用子句形式寫出。

霍恩子句是一類特殊的子句，它被定義為至多包含一個正文字的子句。即當(dāng)上面的子句（1）中，m=1時的子句，表示為：P←Q1,Q2,?,Qn。因此，霍恩子句必須是以下4種形式之一：

① P←Q1,Q2,?,Qn （n不等于0），

② P← （上式中n=0），

③ ←Q1,Q2,?,Qn （n不等于0），

④ □ (上式中n=0)。

其中，我們把①這種形式的霍恩子句稱為一個過程，②這種形式的霍恩子句稱為一個事實，而把③稱為目標(biāo)，④則稱為停機(jī)語句，表示程序執(zhí)行終止。

2.3.2 邏輯程序設(shè)計

可以看出，霍恩子句形式簡明，邏輯意義清晰，最重要的是其消解過程可以與計算機(jī)程序的執(zhí)行過程統(tǒng)一起來，因此研究者們開始將霍恩子句邏輯直接作為程序設(shè)計語言。傳統(tǒng)的程序設(shè)計來說，算法的邏輯意義往往被程序復(fù)雜的控制成分所掩蓋，使程序的正確性難以得到證明。而且通常的高級程序設(shè)計語言屬于過程性語言，需要在程序執(zhí)行前詳細(xì)規(guī)定運行步驟�？仆郀査够鶎鹘y(tǒng)的算法或?qū)τ猛ǔ８呒壵Z言編寫的程序提出了一個著名的分析公式，即算法＝邏輯＋控制。其基本思想是要從根本上改變程序設(shè)計的方法：用戶只

最新搜索

歸納邏輯程序設(shè)計初探2008

光纜專業(yè)高級ok

同濟(jì)86-01外科考研題

2016新人教版一年級語文第一單元練習(xí)卷

下列對評價企業(yè)發(fā)展能力目的的說法不正確的是

公共關(guān)系經(jīng)典案例分析75

[單選題] “知人者智,自知者明”,這句話與下列哪一項內(nèi)容有

三億文庫

39地震勘探

園林亭的布局與位置

  本文關(guān)鍵詞：歸納邏輯程序設(shè)計初探，由筆耕文化傳播整理發(fā)布。