北航程序設(shè)計(jì)語言原理教材第12章

第第#頁第12章邏輯式程序設(shè)計(jì)語言無論是命令式還是函數(shù)式程序都把程序看作是從輸入到輸出的某種映射。當(dāng)然命令式語言有時(shí)沒有數(shù)據(jù)輸出，但也要“輸出”某些動(dòng)作。為了實(shí)現(xiàn)這種映射，程序要對(duì)數(shù)據(jù)結(jié)構(gòu)實(shí)施某個(gè)算法過程，算法實(shí)現(xiàn)該程序功能。算法又是以程序語言提供的控制機(jī)制實(shí)現(xiàn)計(jì)算邏輯。所以，R.Kowalski說：算法=邏輯+控制然而傳統(tǒng)語言計(jì)算邏輯在程序員心里，隱式地體現(xiàn)在程序正文之中，為此程序正確性證明還要把它隱含的邏輯以斷言形式地寫出來。自然人們會(huì)想到能不能把描述計(jì)算的理論基礎(chǔ)命題演算和謂詞演算直接變?yōu)槌绦蛟O(shè)計(jì)語言。這樣，也許不必用求值來判定某件事情的真、偽，直接根據(jù)事實(shí)和規(guī)則判定真?zhèn)危罢页觥苯狻Ｊ聦?shí)上，這是可行的，而且在人工智能的專家系統(tǒng)、語言理解、數(shù)據(jù)庫查詢中非常需要這種程序設(shè)計(jì)語言。1970年誕生的Prolog長(zhǎng)久不衰就是例證。邏輯程序設(shè)計(jì)的基本觀點(diǎn)是程序描述的是數(shù)據(jù)對(duì)象之間的關(guān)系，它的抽象層次更高而不限于函數(shù)(映射)關(guān)系。關(guān)系也是聯(lián)系，對(duì)象和對(duì)象、對(duì)象和屬性的聯(lián)系就是我們所說的事實(shí)。事實(shí)之間的關(guān)系以規(guī)則表述，根據(jù)規(guī)則找出合乎邏輯的事實(shí)就是推理。因此，邏輯程序設(shè)計(jì)范型是陳述事實(shí)，制定規(guī)則，程序設(shè)計(jì)就是構(gòu)造證明。程序的執(zhí)行就在推理，和傳統(tǒng)程序設(shè)計(jì)范型有較大的差異。本章我們從邏輯程序設(shè)計(jì)理論基礎(chǔ)，謂詞演算導(dǎo)出邏輯程序語言的理論模型，并介紹邏輯程序設(shè)計(jì)語言Prolog的主要特征和實(shí)現(xiàn)要點(diǎn)。謂詞演算謂詞演算是符號(hào)化事實(shí)的形式邏輯系統(tǒng)，它也是邏輯程序設(shè)計(jì)語言的模型，謂詞演算在所有計(jì)算機(jī)理論的書籍中均有論述，本章僅簡(jiǎn)單復(fù)習(xí)，主要目的是引入術(shù)語。謂詞演算諸元素用形式方法研究論域上的對(duì)象需要一種語言，它能表達(dá)該域?qū)ο缶哂惺裁葱再|(zhì)(properties)，以及對(duì)象間有些什么關(guān)系(relations)。為了一般化還要有變量(variable)指明域上某個(gè)(些)對(duì)象，以及準(zhǔn)確說明對(duì)象情況的量詞(quantifiers)。當(dāng)然這個(gè)語言還需要一些輔助的符號(hào)(繼承自初等集合論)。描述以公式(Formulas)表達(dá)，即描述一般命題的謂詞。謂詞公式中各元素按一定邏輯規(guī)則變換即謂詞演算(predicatecalculus)。以下是謂詞公式的示例：mXp(X)—存在具有性質(zhì)p的對(duì)象X。VYp(Y)—所有的Y,即域上任何對(duì)象，均具有性質(zhì)p。

VXmY(X=2*Y)—對(duì)于所有的X都可以找到Y(jié),其值為X的一半，其中的邏輯連接”=是中綴表示。等效于=(X,2*Y)。謂詞公式各元素符號(hào)表示法在各教程中不盡相同，謂詞演算的表示由以下元素組成:公式由一組約定的符號(hào)組成的序列，它包括常量(指明域上的某個(gè)對(duì)象)、變量(域上任意對(duì)象)、邏輯連接(指明對(duì)象狀態(tài)及對(duì)象間的關(guān)系，有數(shù)量上的＞、＞=、=、V、＜=、/=和邏輯上的V、A、1、一、＜=＞)、命題函數(shù)(指明對(duì)象間的函數(shù)性質(zhì))，謂詞(對(duì)象間約定的關(guān)系)，量詞(邏輯連接的一種，指明對(duì)象狀態(tài))。一階謂詞演算系統(tǒng)中公式里不得嵌套謂詞。⑵常量指明論域(universeofdiscourse)上的對(duì)象，也是數(shù)學(xué)對(duì)象。通常一個(gè)邏輯系統(tǒng)要引入多個(gè)論域，一般有十進(jìn)制整數(shù)域、真值域、字符域，可用不同的符號(hào)表達(dá)有區(qū)別的域。常量可以看作是退化了的函數(shù)(沒有變?cè)?。常量以字面量或小寫字母表示。變量可束定到特定域上某個(gè)范圍的對(duì)象上，在演算(歸約)期間它可以例化為具體對(duì)象(常量對(duì)象)，變量是數(shù)學(xué)意義的，一旦束定整個(gè)演算期間不變，變量以大寫字母表示。函數(shù)表征對(duì)象具有的映射關(guān)系，函數(shù)帶參數(shù)，從變?cè)蛴成涞浇Y(jié)果值域(可以是不同的域)。變?cè)话闶浅Ａ?、變量、函?shù)結(jié)果值、變?cè)谡Z法上都叫項(xiàng)(term)。函數(shù)以小寫標(biāo)識(shí)符表示。謂詞表征對(duì)象某種性質(zhì)的符號(hào)，謂詞帶上一到多個(gè)變?cè)?對(duì)象)即為斷言(assertion)。它斷言這些對(duì)象具有謂詞所指性質(zhì)，謂詞形如函數(shù)，當(dāng)該變?cè)_實(shí)具有所指性質(zhì)時(shí)隱含真值，否則為假。當(dāng)謂詞應(yīng)用到的變?cè)浅Ａ炕蛞驯皇ǖ淖兞可蠒r(shí)，就叫做句子(senteuce)或命題(proposition)，查詢時(shí)能返回真假值。當(dāng)謂詞應(yīng)用到變量或包含變量的項(xiàng)上時(shí)，它依然是謂詞但不能形成句子，只有例化才能判定真?zhèn)?，形成句子。謂詞變?cè)膫€(gè)數(shù)稱作parity),故有單目、N目謂詞之稱。例12-1N-目謂詞的例子。謂詞目謂詞目odd(X)1father(F，S)2divide(N，D，Q，R)4X是奇數(shù)F是S的父親N除D得商Q和余數(shù)R結(jié)果值False結(jié)果值FalseTureTrueN未例化，不知真假odd(2)divide(23，7，3，2)father(changshan，changping)divide(23，7，3，N)(6)量詞變量可以代表域中任何對(duì)象，量詞可以指定某種集合，量詞有兩個(gè)，一為全稱'V'、一為存在'3'，量詞限定的變量名作用域是整個(gè)公式，它說明同名變量。有些謂詞經(jīng)量詞修飾后即沒有變量，可成句子或命題。結(jié)果值FalseTrueTrue結(jié)果值FalseTrueTrueFalseTrue，如X=3，Y=1False，但很難證明VXodd(X)3Xodd(X)VX(X=2*Y+1—odd(X))VX3Ydivide(X，3，Y，0)3X3Ydivide(X，3，Y，0)3XVYdivide(X，3，Y，0)

例12-3量化公式量化謂詞VXodd(X)mXodd(X)V例12-3量化公式量化謂詞VXodd(X)mXodd(X)VX(X=2*Y+1—odd(X))VX3Ydivide(X,3,Y,0)3X3Ydivide(X,3,Y,0)3XVYdivide(X,3,Y,0)取反TOC\o"1-5"\h\zmXnotodd(X)[1]VXnotodd(X)[2]mXnot(X+2*Y+1—odd(X))[3]3Xnot(X=2*Y+1)orodd(X))[4]3X((X=2*Y+1)andnotadd(X))[5]3XVYnotdivide(X,3,Y,0)[6]VXVYnotdivide(X,3,Y,0)[7]VX3Ynotdivide(X,3,Y,0)[8]第［4］、［5］行實(shí)際就是通過謂詞演算得到更加直觀的等價(jià)式，因?yàn)榫植縩ot是極容易找出例證的。(7)邏輯操作and,or,not,-(蘊(yùn)含)<=>(全等)是最基本的邏輯運(yùn)算符，然而，最本質(zhì)的有and(A),or(V),not(T就夠了，如：A—B=notAorB=—AVBAv=>B=(AandB)or(not(Aand(notB)))=(AAB)V—(AA—B)命題演算即原子命題通過邏輯連接,等價(jià)變換,達(dá)到驗(yàn)證命題真理性的目的。謂詞演算以準(zhǔn)確的謂詞描述論域上對(duì)象的邏輯關(guān)系,通過等價(jià)變換達(dá)到證明一般命題真理性的目的。命題演算是謂詞演算的特例。謂詞演算的等價(jià)變換等價(jià)變換即演繹推理,不同的邏輯連接有其等價(jià)變換的規(guī)則。命題,謂詞演算規(guī)則可以查有關(guān)文獻(xiàn)。本節(jié)演示一般謂詞公式變換為子句的實(shí)例。’卜'號(hào)為“可推出”。［1］以A,V,—如上例消除f、v=>符號(hào)。［2］化為前束范式,消除最外的—符號(hào),即否定符號(hào)內(nèi)移?！?3Xp(X))卜VX(—p(X))［3］利用斯柯林變換消去存在量詞。如：VX3Z(c(Z,X)Ab(X))卜VX(c(z,X)Ab(X))再如：VX(a(X)Ab(X)V3Yc(X,Y))卜VX(a(X)Ab(X)Vc(X,g(X)))(11.1)其中g(shù)(X)是對(duì)任何一X可得到(存在)的Y。［4］消除前束范式的全稱量詞。既然設(shè)定所有變量均為全稱,要不要符號(hào)都是一個(gè)意思,即都要搜索全域才能證實(shí)該變量,則(11.1)式為：卜a(X)Ab(X)Vc(X,g(X))(11.2)［5］利用分配率PV(QAR)=(PVQ)A(PVR)化成合取范式，(11.2)式成為：卜(a(X)Vc(X,g(X))Ab(X)Vc(X,g(X)))(11.3)經(jīng)過以上變換任何一復(fù)合公式均可成為如下形式:F=C1AC2A?Cn(11.4)且其中Ci稱為子句，如果以'，’代替'A',且其次序無關(guān)可表達(dá)為集合形式：F=C1,C2,?,Cn其中Ci內(nèi)部沒有其它邏輯連接符號(hào)，只有'V'。若以';'代'V'則有：Ci=L1VL2V?Lv=L1;L2;?;Lv(11.5)因此，任一公式均可化為'V'連接的子句的集合，證明'V'連接的子句為真是很容易的,但證明整個(gè)公式為真則需所有子句均為真，即子句邏輯。自動(dòng)定理證明自1879年Frege正式研究符號(hào)邏輯以來，至本世紀(jì)30年代末的五十年期間，數(shù)理邏輯發(fā)展比較完備，它們一直用作基礎(chǔ)數(shù)學(xué)的證明系統(tǒng)。電子計(jì)算機(jī)問世后，人們不僅借助計(jì)算機(jī)完成手工不能完成的證明工作(如1987年的四色定理證明)，更感興趣的是用邏輯定理對(duì)程序作正確性的自動(dòng)證明。本節(jié)簡(jiǎn)述證明系統(tǒng)的概念和模型。證明系統(tǒng)用謂詞演算公式描述的事實(shí)即證明系統(tǒng)中的公理(axioms)，證明系統(tǒng)(proofsystem)是應(yīng)用公理演繹出定理(theorems)的合法演繹規(guī)則的集合。所謂演繹，也叫歸約(deduction)，是對(duì)證明系統(tǒng)中合法推理規(guī)則的一次應(yīng)用。在一個(gè)簡(jiǎn)單的演繹步驟中，可以從公理導(dǎo)出結(jié)論(conclusion)，中間可利用以這些規(guī)則演繹出的定理。證明(proof)是個(gè)語句序列，以每個(gè)語句得到證明而結(jié)束，即每個(gè)句子要么演繹成公理，要么演繹成前此導(dǎo)出的定理。一個(gè)證明若有N個(gè)語句(命題)則稱N步證明，反駁(refutation)是一個(gè)語句的反向證明。它證明一個(gè)語句是矛盾的，即不合乎給定的公理。同一命題的正向證明和反駁有時(shí)會(huì)有天壤之別，證明長(zhǎng)度和復(fù)雜性差別很大。構(gòu)造一個(gè)證明或反駁要有深入的洞察、聯(lián)想還要有點(diǎn)靈感。寫得好，脈絡(luò)清晰，句子簡(jiǎn)明，反之臃腫晦澀。即使是較差的證明構(gòu)造起來也要有點(diǎn)技巧。一個(gè)語句若能從公理出發(fā)推演出來，則稱合法語句，任何合法語句也叫做定理(theorem)。從某一公理集合導(dǎo)出的所有定理集合稱為理論(theory)。一般說來，理論具有一致性，它不包含相互矛盾的定理。模型從公理集合中導(dǎo)出定理集稱之為理論，有了理論我們要解釋它的語義必須借助某個(gè)模型(model)。因?yàn)樾问较到y(tǒng)只是符號(hào)抽象，借助模型我們可為每個(gè)常量、函數(shù)、謂詞符號(hào)找到真理性的解釋。即定義每個(gè)論域，并表明域上成員和常量公理之間的關(guān)系。公理的謂詞符號(hào)必須派定為域中對(duì)象的性質(zhì)，函數(shù)派定為對(duì)域中對(duì)象的操作。不一致的理論就沒有模型，因?yàn)闊o法找到同時(shí)滿足相互矛盾定理的解釋。公理集合一般情況下只是定義的部分(偏)函數(shù)和謂詞，是問題域的一個(gè)側(cè)面。所以能滿足該理論的模型往往不止一個(gè)。如，下例是一“間隔數(shù)理論”為找出該理論的一個(gè)模型，先找一個(gè)論域，它必需要能解釋給出的三個(gè)公理，常量'1'和2，函數(shù)符'+',謂詞interval。例12-4一個(gè)最簡(jiǎn)單的理論公理集:TOC\o"1-5"\h\zVXinterval(X)fnotinterval(X+1)(al)VXnotinterval(X+1)finterval(X)(a2)2=1+1(a3)從間隔數(shù)公理可導(dǎo)出定理:VXinterval(X)^interval(X+2)(t1)VXinterval(X+2)finterval(X)(t2)如果我們?cè)O(shè)定論域是整數(shù)，則'1'，'2'可解釋為整數(shù)一和二，且'+'就是整數(shù)加(符合公理a3),即加函數(shù)。謂詞interval間隔數(shù))在整數(shù)域上顯然有兩個(gè)子域odd(奇數(shù))、even(偶數(shù))都能夠滿足。如果奇數(shù)都是間隔數(shù)，在本理論中偶數(shù)定然不是。反之，奇數(shù)不是。既然我們論述在整數(shù)域上，對(duì)任一整數(shù)我們倒反不能確定它是否為間隔數(shù)了，間隔數(shù)理論不能證明interval(3)，也不能證明notinterval?)為真命題。這就是Milbert討論過的可判定性(decidability)問題。1936年Church和Turing證實(shí)謂詞演算可判定性問題是沒有解的，因?yàn)椴淮嬖谝膊豢赡茏C明一個(gè)算法能正確地驗(yàn)證非真命題。對(duì)于真命題即使有算法過程存在，也要在無限長(zhǎng)的時(shí)間才能做完證明。然而，一旦我們斷言interval(3)或interval(2)是真命題，我們立刻可通過演繹證明按這個(gè)理論寫出的每一個(gè)謂詞為真。這就是Goedel和Herbrand1930年證實(shí)的謂詞演算具備的完整性(completeness)。它可以證明該理論所有模型里的每一語句為真。謂詞演算可用來開發(fā)每一邏輯真命題的形式證明系統(tǒng)。甚至存在機(jī)械的證明方法(Gentzen1936)。證明技術(shù)從謂詞演算具有完整性，理論上可作出自動(dòng)生成程序并證明按公理集合建立的任何理論，它們是公理集合的邏輯結(jié)論。但實(shí)際做起來，要找到切題的證明如同大海撈針，效率難以容忍。即使把問題限制在證明單個(gè)命題，關(guān)鍵仍然是效率。如果我們從公理出發(fā)做出每一個(gè)步驟，在新的步驟上仍然要查找每一個(gè)公理找出可能的推理。如此下去就形成一個(gè)龐大的樹行公理集，每層的結(jié)點(diǎn)都是表示一個(gè)公理的語句，其深度和寬度隨問題和最初給出的公理而定，一層一步驟，N層的樹就是N步推理。對(duì)于自動(dòng)定理證明程序，只有窮舉每條可能的證明步驟才能說它是完全的。然而，窮舉完所有路徑馬上遇到組合爆炸問題，無論是深度優(yōu)先還是廣度優(yōu)先，百步演繹可能的路徑數(shù)都是天文數(shù)字。以下是證明路徑示例。例12-5試證65534是個(gè)好整數(shù)設(shè)謂詞good(X)表示X是好整數(shù)。謂詞Powtwo(Y，Z)表示2的Y次方為Z，顯然，powtwo(0，1)是事實(shí)。若A是好整數(shù)與2作整數(shù)運(yùn)算之后結(jié)果仍應(yīng)為好整數(shù)。若2p=A且p為好整數(shù)則A也是好整數(shù)，2p+1=2*A也都是顯然的公理。所以有：公理f1good(0)f2powtwo(0，1)

r3good(A-2)Jgood(A)r4good(A+2)Jgood(A)r5good(A*2)Jgood(A)r6good(A)jpowtwo(P,A),good(P)r7powtwo(P+1,A*2)jpowtwo(P,A)s1good(2)f1和r4s2good(4)s1和r5s3powtwo(1，2)f2和r7s4powtwo(2，4)s3和r7s5powtwo(3，8)s4和r7s6powtwo(4，16)s5和r7s7good(16)s2，s6和r6s8powtwo(5，32)s6和r7s9powtwo(6，64)s8和r7s10powtwo(7，128)s9和r7s11powtwo(8，256)s10和r7s12powtwo(9，512)s11和r7s13powtwo(10，1024)s12和r7s14powtwo(11，2048)s13和r7s15powtwo(12，4096)s14和r7s16powtwo(13，81926)s15和r7s17powtwo(14，16384)s16和r7s18powtwo(15，32768)s17和r7s19powtwo(16，65536)s18和r7s20good(65536)s7,s19和r6s21good(65534)s20和r3七條公理中有兩個(gè)事實(shí)5條規(guī)則,以下證明過程:得證這個(gè)證明人工花了21步,機(jī)器怎么會(huì)知道？它必須把每個(gè)事實(shí)和已證明的定理逐個(gè)代入到這5個(gè)規(guī)則中驗(yàn)證得出新的定理，每得出一個(gè)powtwo(p+1,A*2)后要像第七步s7和第二十步s20一樣把幕和值分出來，連試探到計(jì)算至少要操作721=4.7173X1017次(4.72億億次)。歸結(jié)定理證明不加限制地寫出公理,窮舉證明顯然不是一條自動(dòng)證明的出路。因?yàn)橐獧C(jī)器自動(dòng)查匹配演算到預(yù)期的合適公式,代價(jià)是極大的。于是對(duì)謂詞公式的寫法加以限制,即在12.1.2節(jié)把任何公式化為子句邏輯的辦法可以省去一大片的歸約演算,即使如此,窮舉證明計(jì)算量也相當(dāng)可觀。一個(gè)技術(shù)是J.A.Robinson1965年提出的歸結(jié)(resolution)法，歸結(jié)法是命題演算中對(duì)合適公式的一種證明方法。為了證明合適公式F為真，歸結(jié)法證明「F恒假來代替F永真。歸結(jié)原理是:設(shè)有前題LVP和「LVR則其邏輯結(jié)論是PVR，因?yàn)閮蓚€(gè)子句中含有一個(gè)命題的正逆命題(L，「L)。若L為真「L一定為假，P若為真，PVR也為真。若L為假「L為真，P若為真，PVR也為真。這個(gè)推理把兩子句合一(unification)并消去一對(duì)正逆命題，故歸結(jié)也譯作消解。歸結(jié)證明

的過程并稱之歸結(jié)演繹，其步驟如下:把前題中所有命題換成子句形式。取結(jié)論的反，并轉(zhuǎn)換成子句形式，加入[1]中的子句集。在子句集中選擇含有互逆命題的命題歸結(jié)。用合一算法得出新子句(歸結(jié)式)再加入到子句集。重復(fù)[3]，若歸結(jié)式為空則表示此次證明的邏輯結(jié)論是矛盾，原待證結(jié)論若不取反則恒真。命題得證。否則繼續(xù)重復(fù)[3]。例12-6歸結(jié)證明若有前題待證命題取反得新子句若有前題待證命題取反得新子句TOC\o"1-5"\h\zplQV「Pp5Pp2RV^Qp6Up3SV「Rp4「UV「S取待證命題的反，得PAU，它是人連接的兩個(gè)子句P,U,把它們加到前題子句集，為p5，p6。歸結(jié)演繹如下圖:QV「PPQRQV「PPQRV「Q「Sp1-p5歸結(jié)再與p2歸結(jié)再與p3歸結(jié)再與p4歸結(jié)再與p6歸結(jié)由于歸結(jié)為空，則「PV「Q得證。由本例可以看出兩個(gè)問題，第一，歸結(jié)法是由合一算法實(shí)現(xiàn)的。所謂合一是找出行式匹配的兩子句，將它們合一為歸結(jié)式，相當(dāng)于代數(shù)中的化簡(jiǎn)。更廣義的合一算法是找出兩子句最通用的實(shí)例(對(duì)于謂詞演算)即找出變量的實(shí)例，使兩子句等價(jià)。例如:公式1公式2廣義合一pp(a,b)pp(X,Y)X=a,Y=b;p(a,b)Aq(c,d)p(X,Y)Aq(Z,W)X=a,Y=b,Z=c,W=dq(p,g(X,Y),X，Y)q(Y,Z，h(U，k),U)U=Y=p，X=h(p,k)Z=g(h(p,k),p)第二是如果得不出矛盾那么歸結(jié)法要無休止地做下去，中間歸結(jié)式出得越多，匹配查找次數(shù)越多,每一步都做長(zhǎng)時(shí)間計(jì)算,顯然,要想出比這種原始?xì)w結(jié)法的更好辦法,即利用切斷(cut)操作，并對(duì)子句形式進(jìn)一步限制的超級(jí)歸結(jié)法(Hyperresolution)。Horn子句實(shí)現(xiàn)超歸結(jié)Horn子句是至多只有一個(gè)非負(fù)謂詞符號(hào)的子句。這就等于說，通過謂詞演算一個(gè)語句只包含一個(gè)蘊(yùn)含運(yùn)算符連接前題和結(jié)論，前題是由’人'連接的幾個(gè)謂詞，結(jié)論就是單一的謂詞符號(hào)。Horn子句形式示例如下：WT(12.6)其中只有一個(gè)非負(fù)謂詞S,可作以下演算，先將S移向右方卜WT(12.7)按德?摩根定律卜SV^(PAQARAT)(12.8)'V^'即'一',貝I」卜Sj(PAQARAT)(12.9)此即條件Horn子句，因?yàn)?12.9)的意義是if(PAQARAT)thenS。顯然，若S為空，則為無條件Horn子句，是一個(gè)斷言(事實(shí))。超級(jí)歸結(jié)實(shí)質(zhì)上是將無條件Horn子句中的謂詞符號(hào)和條件子句中的對(duì)應(yīng)謂詞符號(hào)合一。找出所有子句中變量的實(shí)例集，使每一條件子句為真。如果不滿足貝尋找新的實(shí)例(回溯算法)，如果滿足了也要找出所有實(shí)例。為了消去不必要的匹配以提高超級(jí)歸結(jié)的效率，cut操作是必須的，它可以由程序員指定。當(dāng)找到一個(gè)解之后不再搜索其它解。它本身是個(gè)無變?cè)^詞，當(dāng)執(zhí)行到它時(shí)，不再回溯。cut操作也可用于分情形動(dòng)作控制與fail(失敗)謂詞聯(lián)用，12.4節(jié)還將舉例。邏輯程序的風(fēng)格基于自動(dòng)定理證明的邏輯語言，有其獨(dú)特的程序設(shè)計(jì)風(fēng)格，因?yàn)樗幻枋鲇?jì)算過程而是描述證明過程。例如，有一個(gè)問題：對(duì)數(shù)組A按升序排序，我們?cè)鯓泳庍壿嫵绦蚰兀课覀冎缓脴?gòu)造一個(gè)和A那樣大的數(shù)組B,而且它是排好升序的，我們證明命題：“存在一個(gè)數(shù)組B它是數(shù)組A重排升序”為此，可以陳述更嚴(yán)謹(jǐn)一些：B是A的重排，當(dāng)且僅當(dāng)B的元素就是A的元素，且B[i]vB[j],ivj。于是，自動(dòng)定理證明系統(tǒng)依靠環(huán)境，構(gòu)造一個(gè)希望的解(B)，并證明它的存在。構(gòu)造的辦法不外乎匹配查找，例化或置換。證明是本題的主旨排序成了副產(chǎn)品！除了證明性風(fēng)格而外，邏輯程序的第二個(gè)特點(diǎn)是描述性，請(qǐng)見下例：例12-7求平均成績(jī)的邏輯程序打開一分?jǐn)?shù)文件scores，讀入分?jǐn)?shù)求和并用的數(shù)N除之得平均成績(jī)。average：-see(scores)，getinput(Sum，N)，seen(scores)，AvisSum/N，print('Average='，Av)getinput(Sum，N)：-ratom(X)，not（eof），getinput（Sum1，N1），SumisSum1+X，NisN1＋1.getinput（0，0）:-eof.要使求平均成績(jī)程序正確，必先打開（see）文件，從中得到輸入，得N個(gè)數(shù)的總和記以N和Sum,關(guān)閉（seen）文件后求平均值A(chǔ)v，打印之。至于如何得到Sum和N,細(xì)化謂詞getinput（_,_）。若要getinput成立，先讀入一原子X（ratom是系統(tǒng)提供的謂詞）。若未至文件末尾，讀其余分?jǐn)?shù)并求和。getinput是遞歸定義，并相應(yīng)斷言Sum，N和Sumi，N1的關(guān)系。如果已至文件結(jié)束標(biāo)記eof則輸入為（0，0）。這個(gè)程序?yàn)榍笃骄謹(jǐn)?shù)給出三條規(guī)則，‘，‘號(hào)即子句的'人'連接，意即所有子句為真，左端謂詞才成立。這個(gè)程序是用Prolog寫的，我們雖未介紹它的語法，一經(jīng)簡(jiǎn)單解釋我們即可讀懂該程序。它的風(fēng)格是：若要A成立，做B,做C,做D，…再細(xì)化，若要B做出則要做P，做Q,做R,…這與過程式語言自頂向下描述沒什么差別，且比較自由，沒有嚴(yán)格的順序性。當(dāng)然程序執(zhí)行還需有事實(shí)的陳述，以及需求證明的查詢。邏輯程序第三個(gè)特點(diǎn)是大量用表和遞歸實(shí)現(xiàn)重復(fù)操作，遞歸特別利于謂詞描述，我們只要能說明特征謂詞的一步動(dòng)作為真，其余如法炮制，程序就設(shè)計(jì)完了，上例中，getinput，讀一數(shù)X,求和并令門數(shù)加1,其余照做。關(guān)于表與遞歸聯(lián)用的例子，見12.4節(jié)中Prolog的例子。12.4典型邏輯程序設(shè)計(jì)語言PrologProlog是典型的邏輯程序設(shè)計(jì)語言，它基于一階謂詞邏輯，直接陳述問題世界的事實(shí)、規(guī)則和目標(biāo)，非常簡(jiǎn)明清晰，所以人們稱之為自文檔的。Prolog的程序?qū)⑦壿嫼涂刂骑@式分離，它使程序正確性證明簡(jiǎn)化（只涉及知識(shí)，即邏輯部分），程序的優(yōu)化（只涉及控制部分）不影響程序正確性，是正交設(shè)計(jì)成功的范例。Prolog的環(huán)境Prolog很長(zhǎng)一段時(shí)間都是交互式語言，它必須要有支持環(huán)境，即管理事實(shí)和規(guī)則的數(shù)據(jù)庫，并為操縱它們提供元語言。小的數(shù)據(jù)庫可以文件形式聯(lián)接上，大的庫在鍵盤上調(diào)用輸入函數(shù)consult（filename）。一旦進(jìn)入系統(tǒng)，即可查看庫內(nèi)容（用listing（predicate_name））或編輯它們（用retract（z））,還可以擴(kuò)充數(shù)據(jù)庫（用asserta（X）或assertz（X））。聯(lián)上數(shù)據(jù)庫，程序員即可交互使用。查詢、測(cè)試假設(shè)、斷言更多的事實(shí)。為響應(yīng)查詢，Prolog系統(tǒng)執(zhí)行它的證明過程并查找能滿足查詢變量的事實(shí)集。查找成功，寫出找到的事實(shí)，若程序員滿意并打回車鍵后，系統(tǒng)給出“yes”并顯示新提示，如果數(shù)據(jù)庫查完還未找到要的事實(shí)則給出“no”，并顯示新提示。數(shù)據(jù)對(duì)象和項(xiàng)Prolog的基本成分是對(duì)象（常量、變量、結(jié)構(gòu)、表）、謂詞、運(yùn)算符、函數(shù)、規(guī)則。?常量預(yù)定義有十進(jìn)制整數(shù)，用戶定義的常量叫原子，有小寫字母開頭的名字，Prolog是無類型的，程序是理論，可以對(duì)應(yīng)多個(gè)模型（也可以沒有），因而原子在不同模型中是不同的對(duì)象。?變量大寫字母開頭的名字。一個(gè)規(guī)則中同一變量名都將束定到同一對(duì)象上。符號(hào)‘_'是變量的占位符，對(duì)于確有一變量但暫時(shí)不能指明時(shí)則補(bǔ)上‘_'，一個(gè)規(guī)則中，‘_'出現(xiàn)幾次就束定幾個(gè)變量。?結(jié)構(gòu)復(fù)合的數(shù)據(jù)結(jié)構(gòu)，如記錄類型可用函子（函數(shù)名）和括在括號(hào)中的成分（域）表給出:＜函數(shù)名＞（＜成分＞，?，＜成分＞）例如，course（C_no，C_name，Teacher，Precno）?表表是最頻繁使用的數(shù)據(jù)結(jié)構(gòu)。以方括號(hào)表示，［］（空表），［HeadITail］（遞歸定義的一般表）［X,Y,Z］（定長(zhǎng)表）［a，bIZ］（表頭為常量，表尾為變量Z）。表中元素叫項(xiàng)（term）可以是原子、表、空。表的規(guī)格說明有兩種形式，它們等效:［X，Y，Z］?（x,?y,?（z,［］））［Head，Tail］?（Head,Tail）//'?'指出連接關(guān)系開端表（open）是表尾長(zhǎng)度可變的表。證明過程中，開端表可以和任何與其表頭有相同常量的表匹配（合一）。選擇子函數(shù)head（X），tail（X）可操縱表X返回表頭或表尾變?cè)?謂詞預(yù)定義有=、\=、＜、=＜、＞、=＞。用戶可定義自己的謂詞，以小寫字母給出謂詞名。機(jī)器是不理解謂詞的語義的，它只知道匹配，所以，程序員應(yīng)將謂詞的意義記清并按它寫程序。謂詞帶參數(shù)，即項(xiàng)，但參數(shù)不能是謂詞、函數(shù)和關(guān)系。?運(yùn)算符預(yù)定義了整數(shù)運(yùn)算符+、-、*、/和mod，可以寫成標(biāo)準(zhǔn)的函數(shù)式+（3，x）也可以寫成中綴形式3+x,使用中綴形式時(shí)有通常的優(yōu)先級(jí)，算術(shù)等式還有一種is的形式，如Xis（A+B）modC,當(dāng)Prolog處理這樣的公式時(shí)，它用A,B,C的當(dāng)前束定來執(zhí)行這個(gè)計(jì)算其返回值束定于X,如is右邊變量未束定值則返回錯(cuò)誤。從純語法意義上Prolog的項(xiàng)什么都可以表示：＜項(xiàng)＞：：=＜常量＞|＜變量＞|＜結(jié)構(gòu)＞|（＜項(xiàng)＞）|＜表＞＜后綴算符〉lv項(xiàng)＞＜中綴算符＞＜項(xiàng)＞|v,項(xiàng)＞＜前綴算符〉從語義角度，以下語法描述提供了處理時(shí)的語義概念：＜程序〉?＜子句〉＜子句〉f（v事實(shí)〉|＜規(guī)則〉|＜查詢〉）＜事實(shí)〉f＜結(jié)構(gòu)〉＜規(guī)則〉f＜頭＞:-＜體＞＜頭＞f＜結(jié)構(gòu)〉＜體＞f＜目標(biāo)〉，＜目標(biāo)〉＜目標(biāo)〉f/*形如p或q（T,?,）的字面量*/Prolog程序結(jié)構(gòu)Prolog程序由子句組成，如前所述，子句模型是Horn子句。Horn子句本質(zhì)上提供最基本的形式邏輯，即if_then條件推理，把多個(gè)子句放在條件中，當(dāng)條件(即前題)均滿足，then部分即結(jié)論。如果條件為空，即只有以謂詞表達(dá)的結(jié)論，就是斷言，即事實(shí)。條件子句即為規(guī)則。為了簡(jiǎn)明，Prolog以’:-代替'以'，'代替'and'，以';'代替'or'，'!'代替cut。和其它語言環(huán)境一樣，系統(tǒng)配備了一批支持程序設(shè)計(jì)的預(yù)定義謂詞(相當(dāng)于其它語言的內(nèi)定義函數(shù))。和其它語言一樣，程序分兩部分，定義和應(yīng)用。程序定義該程序所需的公理集，即事實(shí)和規(guī)則。應(yīng)用部分即查詢，即寫出待證的目標(biāo)。整個(gè)程序是一證明系統(tǒng)。(1)事實(shí)與規(guī)則Prolog程序先定義公理集，我們看下例：例12-8Prolog的規(guī)則和事實(shí)條件子句(規(guī)則)pretty(X):-artwork(X)pretty(X):-color(X，red)，flower(X).watchout(X):-sharp(X，_).無條件子句(事實(shí))color(rose，red).sharp(rose，stem).sharp(holly，leaf).flower(rose).flower(violet)artwork(painting(Monet，haystack_at_Giverny)).一般說來，一個(gè)謂詞可以定義好幾個(gè)規(guī)則來表達(dá)它。如同每個(gè)規(guī)則用‘or'聯(lián)接起來表達(dá)這個(gè)謂詞，只有一個(gè)(第一個(gè)滿足該謂詞的)規(guī)則來解釋對(duì)該謂詞的調(diào)用。所以可以寫出一系列的規(guī)則來表達(dá)通用的條件語義結(jié)構(gòu)。規(guī)則可以遞歸，這樣就可以實(shí)現(xiàn)算法需要的重復(fù)。當(dāng)然，遞歸謂詞必須至少要有兩條規(guī)則，一為歸納基礎(chǔ)，一為遞歸步驟。查詢Prolog中查詢(query)是要求Prolog證明定理。因?yàn)樘岢龅膯栴}就是證明過程的目標(biāo)，所以查詢也叫目標(biāo)(goal)。語法上查詢是個(gè)由逗號(hào)分開的項(xiàng)表。語義上是同時(shí)滿足的謂詞，逗號(hào)即and。如果查詢中沒有變量，Prolog從已給定的規(guī)則和事實(shí)證明它，查詢以'?-'開始，請(qǐng)看下例：例12-9Prolog的查詢?-pretty(rose).yes?-pretty(Y).Y=painting(Monet，haystack_at_Giverny).Y=rose.no?-pretty(W)，sharp(W，Z)W=roseZ=stemno第一個(gè)查詢問”玫瑰美麗嗎？”它到例12-8的事實(shí)庫中找出玫瑰是花，顏色是紅的，滿足第二條規(guī)則，故查詢結(jié)果是yes。如果查詢中包含變量，Prolog的定理證明系統(tǒng)將找出滿足查詢的實(shí)例集合，查詢中的所有變量均隱含具有量詞，也就是查詢問的是否存在滿足子句的對(duì)象。它給出一個(gè)就等待，當(dāng)程序員鍵入’;'，它就給出下一個(gè)直至沒有，給出no。例12-9中的?-pretty（Y）查詢，它找到例12-8中第一條規(guī)則匹配，再找到最后一個(gè)事實(shí)匹配，找出Y=莫奈的油畫《吉縵尼的草堆》。第二次再查，找出玫瑰。第三次查不出則給出no。查詢所包含的謂詞項(xiàng)，它將自左至右依次處理。僅當(dāng)任何一謂詞項(xiàng)均不滿足才夭折本次處理過程。在這種處理中，前項(xiàng)結(jié)果“好象”對(duì)后項(xiàng)有效和過程語言非常相似。例12-10最大公約數(shù)的歐基里得算法最大公約數(shù)歐基里得算法可用三條規(guī)則描述:gcd（A，0，A）.gcd（A，B，D）:-（A>B），（B>0），RisAmodB，gcd（B，R，D）.gcd（A，B，D）:-（A<B），gcd（B，A，D）.其中A,B是輸入?yún)?shù)，D是輸出參數(shù)。第三條規(guī)則的執(zhí)行，非常象if（AvB）thengcd（B，A，D）。當(dāng)測(cè)試（AvB）為真時(shí)調(diào)用謂詞gcd（B，A，D）。如果成功結(jié)果值束定于D。第二條規(guī)則相當(dāng)于執(zhí)行了兩次if測(cè)試，做一次賦值（將AmodB束定于R），再做一次謂詞匹配，結(jié)果值束定于D。封閉世界內(nèi)的演繹過程查詢建立了演繹過程的目標(biāo)，它以項(xiàng)的邏輯“與“連接給出。Prolog逐一滿足查詢中的各個(gè)子目標(biāo)。子目標(biāo)也可以是含變?cè)闹^詞，它首先到數(shù)據(jù)庫中查變?cè)獋€(gè)數(shù)（目）相同的規(guī)則頭，如果找到，則暫時(shí)列出匹配的變?cè)獙?shí)例。接著處理規(guī)則體的另一個(gè)子目標(biāo)?？凑页龅膶?shí)例能否滿足新的子目標(biāo)，如果成功，繼續(xù)匹配下一個(gè)子目標(biāo)，直到所有子目標(biāo)均滿足。因?yàn)楦髯幽繕?biāo)是“與”的關(guān)系。如果有某個(gè)子目標(biāo)查遍數(shù)據(jù)庫也找不到能滿足的事實(shí)，該子目標(biāo)失敗，但不等于整個(gè)目標(biāo)的失敗，它就回溯到上一個(gè)子目標(biāo)重選事實(shí)繼續(xù)匹配。這種回溯的執(zhí)行過程和例題我們?cè)诘?.4.2節(jié)（2）中已介紹過了。即使是整個(gè)目標(biāo)最后失敗，也不等于這個(gè)目標(biāo)追求的命題是否定的，因?yàn)橄抻跀?shù)據(jù)庫存放的規(guī)則和事實(shí)有限，它是“封閉世界假說”之下的失敗?；厮菔窃跇湫心Ｐ椭乱赃f歸下降法自動(dòng)進(jìn)行的，也就是說，Prolog實(shí)現(xiàn)程序計(jì)算的算法相對(duì)固定。程序員也就沒有必要對(duì)程序作出什么顯式的控制，它的程序控制是隱式的。提高程序質(zhì)量就在于程序員如何安排一個(gè)規(guī)則內(nèi)條件的次序了，各規(guī)則之間的次序并不重要。這是因?yàn)樗扇〉氖巧疃葍?yōu)先，窮舉搜索，不到整個(gè)數(shù)據(jù)庫按規(guī)則子目標(biāo)所有可能的組合全部查完是不能說出fail（失?。┑摹：瘮?shù)和計(jì)算Prolog解題是模型一個(gè)系統(tǒng)，從輸入開始以某種給定的形式希望能導(dǎo)出輸出。對(duì)于其它語言這洽好是定義一個(gè)從輸入到輸出的函數(shù)，設(shè)計(jì)算法（安排對(duì)數(shù)據(jù)結(jié)構(gòu)的加工步驟），做過程式程序設(shè)計(jì)。Prolog是公理化的語言，它只以公理化的方式描述輸出結(jié)果，并用證明過程代替?zhèn)鹘y(tǒng)的計(jì)算過程，即它找出數(shù)據(jù)庫中具有和所希望輸出的對(duì)象有同樣性質(zhì)的對(duì)象，證明它們是一致的。然而，作為一個(gè)程序設(shè)計(jì)語言它也要有最低限度的計(jì)算。（1）函子完成邏輯設(shè)計(jì)中的計(jì)算Prolog為整數(shù)預(yù)定義了五種運(yùn)算符，它們都是計(jì)算函數(shù)，所以，函子以結(jié)構(gòu)形式出現(xiàn)，如:中綴表示前綴表示X+Y*Z+（X，*（Y，Z））A-B/C-（A，/（B，C））中綴和前綴表達(dá)等效，前綴表達(dá)雖可按謂詞理解，兩變?cè)哂?、-、*、/、mod關(guān)系，但它不求真值而有求值結(jié)果，所以，它不是謂詞僅僅是一特殊的結(jié)構(gòu)：＜函數(shù)名＞（＜變?cè)荆?，＜變?cè)荆?。函?shù)求值的的結(jié)果一般通過謂詞is（v變?cè)?，＜表達(dá)式〉）束定到變?cè)?，也可以寫成中綴。它的意思是表達(dá)式（復(fù)合的函子結(jié)構(gòu)）計(jì)算的值返回到變?cè)?，該變?cè)员磉_(dá)式的值實(shí)例化。所以，若要做計(jì)算，一條規(guī)則中至少要有一個(gè)is子句，前述最大公約數(shù)程序的第二條規(guī)則：gcd（A，B，D）;-（A＞B），（B＞0），RisAmodB，gcd（B，R，D）.其中AmodB就是計(jì)算余數(shù)的，計(jì)算后以返回值例化R,再代入后邊的遞歸謂詞。用戶定義的帶數(shù)值計(jì)算的謂詞，必須增加一個(gè)存放返回值的變量。如求最大公約數(shù)的歐基里德算法是兩數(shù)（變?cè)┹氜D(zhuǎn)相除，只要兩個(gè)變?cè)?。上式gcd（A，B，D）變?cè)?個(gè)，D就是為了返回值，是gcd的輸出變?cè)?。把函?shù)改寫為約束，很容易寫出program程序，請(qǐng)看下例12-11求斐波那契數(shù)的Prolog程序斐波那契函數(shù)以下述公式生成以下數(shù)列：1，1，2，3，5，8，13，21，?Fib（0）=1Fib（1）=1Fib（n）=Fib（n-1）+Fib（n-2）編制Prolog程序時(shí)這樣分析：第一、二式是事實(shí)也是公理，把結(jié)果值作為變?cè)諏?。第三式說明，若n為斐波那契數(shù)，n-1和n-2的斐波那契必須成立，且這兩個(gè)數(shù)之和是n的斐波那契數(shù)，n＞1。于是有Prolog程序：Fib（0，1）.Fib（1，1）.Fib（n，f）：-Fib（m，g），F(xiàn)ib（k，h），misn-1，kism-1，fisg+h，n＞1.當(dāng)有查詢?-Fib（5,f）時(shí)，f返回8。（2）邏輯程序的算法表達(dá)算法怎樣用公理表達(dá)呢？我們拿一個(gè)最典型的Quicksort分類程序討論。分類在表上進(jìn)行。我們可以按快速分類寫出它的公理。TOC\o"1-5"\h\zquicksort（未分類表，分類完的表）:-（從未分類表拿出第一元素，以它為基準(zhǔn)，分成兩個(gè)表），[1]quicksort（小表，分類完小表），[2]quicksort（大表，分類完大表），[3]append（分類完小表，基準(zhǔn)元素和分類完大表，分類完總表）[4]這樣把快速分類的總目標(biāo)變成了四個(gè)子目標(biāo)，第二、三個(gè)子目標(biāo)顯然清楚，繼續(xù)遞歸分類。第四個(gè)是以連接謂詞append把它們連成一個(gè)分完類的總表輸出。第一個(gè)子目標(biāo)是將一個(gè)表分解為兩個(gè)表，我們細(xì)化如下：先構(gòu)造一個(gè)“劈分“謂詞，split（基準(zhǔn)元素，未分表，小于基元的表，大于基元的表）。前兩變?cè)斎?，后兩個(gè)輸出。謂詞意義明顯，但算法過程還沒說清如何分。于是，我們從待分類表拿出第一元素，若小于基元素放入小表，否則放入大表，接著再重復(fù)直至都成為空表。最后的Prolog代碼如下例：例12-12快速分類的Prolog代碼r1split(_，［］，［］，［］).r2split(Pivot，［Head|Tail］，［Head|Sm］，Lg)：-Head<Pivot，split(Pivot，Tail，Sm，Lg).r3split(Pivot，［Head|Tail］，Sm［Head|Lg］)：-Pivot<Head，split(Pivot，Tail，Sm，Lg).r4quicksort(［］，［］).r5quicksort(［Head［］］，Head).r6quicksort(［Pivot|Unsorted］AllSorted)：-split(Pivot，Unsorted，Small，Large),quicksort(Small，SmSorted)，quicksort(Large，Lgsorted),append(SmSorted，［Pivot|LgSorted］，AllSorted)。規(guī)則rl,r4雖然是遞歸到頭的一條公理，但也起到聲明數(shù)據(jù)結(jié)構(gòu)的作用。請(qǐng)注意從表中取出元素的技巧，人為寫上［HeadITail］它將表的第一元素束定到名字Head，其余部分束定到Tail名字上，由此分出Pivot，Head直至遞歸分完。規(guī)則r2,r3的'＜謂詞，是實(shí)現(xiàn)條件選擇很典型的方法，規(guī)則r5是處理只有一項(xiàng)的表的特殊情況。（3）邏輯和控制分離Prolog無通常意義的控制結(jié)構(gòu)，也就是該程序動(dòng)作次序（顯然也有）和計(jì)算的子句邏輯沒有必然的關(guān)系。例如，把例12-12中，r4,r5,r6寫在rl,r2,r3前面并不影響本程序的執(zhí)行結(jié)果。如有查詢它總是從第一個(gè)規(guī)則到最后一個(gè)規(guī)則查找匹配。但是，寫得好與不好卻影響效率。為了效率總是把易于找到匹配的規(guī)則寫在最上面。控制優(yōu)化可以大為改善效率。程序邏輯和控制的無關(guān)性決定了邏輯程序設(shè)計(jì)方便易行：先分析程序邏輯，解決正確性問題。再分析程序效率，優(yōu)化控制，使程序完善。但要注意，一味追求高效會(huì)喪失易讀性。例如，例12-12中，r1,r4是到達(dá)遞歸邊界的規(guī)則，完全可以放在r3,r6之后。但r1,r4有表達(dá)數(shù)據(jù)結(jié)構(gòu)的功用，如r1是有一個(gè)變量，三個(gè)表作變?cè)闹^詞公理。一上來就是r2倒反看不清晰。所以，例12-12是遞歸邏輯程序慣用的寫法。cut和not謂詞如前所述，超級(jí)歸結(jié)依賴cut（割斷）操作使歸結(jié)證明人為截止，因?yàn)镻rolog的歸結(jié)模型只能完整地證明正命題，是否有解無法判定。如果明知繼續(xù)下去沒什么意思了就人為截?cái)唷ｏ@然，一旦提供了這個(gè)機(jī)制，它是一雙面刃，用得不好會(huì)破壞證明系統(tǒng)的完整性。（1）安全cut非形式解釋cut，它如同一籬笆，由程序員任意置放在規(guī)則之中，以停止無意義的回溯。例如，有如下規(guī)則：P：-Q，R，S，!T，U，V證明系統(tǒng)首先查找Q、R、S的條件合一，Q滿足R不滿足則回溯改Q,如此下去直至S也滿足，控制經(jīng)！傳到T,此時(shí)滿足Q、R、S的變量實(shí)例均予凍結(jié)?；厮葜荒茉赥、U、V之間，

所有條件均滿足本規(guī)則成功，否則失敗，并不再回溯修改！號(hào)左邊變量實(shí)例。所謂安全cut即不可能導(dǎo)致可證明的目標(biāo)失敗，且大為改善效率。例12-13安全cut示例求1到N的整數(shù)之和r1sum_to（N，1）:-N=1，！.r2sum_to（Nr2sum_to（N，R）:-N1isN-1，當(dāng)有查詢:?-sum_to（1，X）X=1;no?-sum-to（6，X）X=21;sum_to(N1，R1)，RisR1+N.〃匹配r1//打';'號(hào)由于有！不致無限查找第2個(gè)〃匹配r1失敗，匹配r2連續(xù)r2//直至成功，打';'號(hào)也不再找no其實(shí)本例r1寫作事實(shí)sum-to(1,1).也可以求出，但本例寫做規(guī)則，它就要找右端子句匹配，當(dāng)用戶鍵入’「號(hào)時(shí)，如果沒有'！'，它將無限運(yùn)行以查找第二個(gè)滿足sum_to(1，X)的解。實(shí)際是不可能找到的。(2)cut實(shí)現(xiàn)not操作在歸結(jié)證明系統(tǒng)中，一般要求規(guī)則和查詢都用非反條件，盡管not操作完全可以代替cut且程序行文中可讀性更好，但用not時(shí)必須仔細(xì)，因?yàn)樗莄ut實(shí)現(xiàn)的，其定義如下：r1not(X):-X，！，fail.r2not(_).其語義是：若X為'假'貝I」條件not(X)成功。若X成功，not(X)失敗。其推理過程是：?若X為假，匹配r1，在未達(dá)到！時(shí)已失敗，則匹配規(guī)則r2,由于r2什么變?cè)伎梢郧铱倿槌晒?，所以，not(X)是成功的。?若X為真，匹配r1后，X為真，控制通過！傳到fail,則r1失敗。于是回溯到！過不去，只好失敗。由于用了!就地失敗，它不再匹配r2,故not(X)為假。正是由于這個(gè)原因，謂詞p和not(not(p))求值結(jié)果不能保證一樣，有時(shí)not(p)和not(not(p))求值結(jié)果倒是一樣的，以下是not謂詞出毛病的例子：例12-14不可靠的not謂詞假定一規(guī)則test有以下定義：test(S，T)：-S=T.運(yùn)行以下查詢時(shí)有：?-test（3，5）no?-test（5，5）yes?-not（test（5，5））no?-test（X，3），RisX+2.X=3R=5?-not（nottest（X，3））），RisX+2.！errorinarithmeticexpression：notanumber由于第二次not(外部的)求值時(shí)用到上例規(guī)則r1,其中X是not(test(X,3))的結(jié)果值，故X+2不是數(shù)加2。這個(gè)問題原因在于子句邏輯的不可判定性。即我們有時(shí)可以證明理論T,有時(shí)可以證明它的反，notT,有時(shí)兩者均不可證明。如果是后者，說明定理只適用于某些模型而對(duì)另一些模型不能用。我們不能因不能證出T為真而斷言T為假，但Prolog確是這樣，不能證明T為真則斷言not(T)成功。所以，使用not要特別小心。(3)不安全的cut在人工智能領(lǐng)域的啟發(fā)式策略中，證明樹有時(shí)極其龐大，程序員就要割掉部分明知無解的推理樹，有時(shí)由于機(jī)器太慢，樹雖不大，時(shí)間太長(zhǎng)還非這樣做不可。但程序員稍有疏忽就會(huì)釀成大錯(cuò)，把僅有的解都割了去。這時(shí)就破壞了證明完整性。cut使我們處于兩難的境地，它的高效是以風(fēng)險(xiǎn)為代價(jià)得到的，如同60年代goto技巧對(duì)非結(jié)構(gòu)化程序。只要模型是超級(jí)歸結(jié)，cut的兩面性是不可以解決的。12?5Prolog評(píng)價(jià)Prolog提供一種證明風(fēng)格的聲明式程序設(shè)計(jì)，推理清晰，概括能力強(qiáng)，程序和數(shù)據(jù)沒有明顯分離。在復(fù)雜的人工智能程序中，簡(jiǎn)明的表達(dá)有利于程序員寫出好程序。特別是邏輯和控制分開的正交性簡(jiǎn)化了正確性證明，因?yàn)槌绦騿T只需關(guān)注證明的邏輯部分，而優(yōu)化控制提高效率并不影響證明的正確性。Prolog程序具有自文檔性，由于論域直接就是問題域，謂詞清晰描述了論域?qū)ο蟮奶卣髋c關(guān)系，而實(shí)現(xiàn)是單一的遞歸下降匹配算法。沒有影響描述的過多實(shí)現(xiàn)細(xì)節(jié)，自文檔性好是必然的。它的非過程性和沒有“隱藏的語義”使程序更具有安全性。即程序員控制整個(gè)程序比較方便，且不需了解更多實(shí)現(xiàn)細(xì)節(jié)。在程序員尚不清楚如何組織數(shù)據(jù)和計(jì)算過程的應(yīng)用中，Prolog有極大優(yōu)勢(shì)，因?yàn)樗C明的是后果而不是過程，且對(duì)程序的順序性要求不嚴(yán)。只陳述應(yīng)如何如何，要如何如何，并未詳細(xì)安排計(jì)算過程。正是由于非過程性，它也成為潛在的并行程序設(shè)計(jì)語言的候選者，所以，當(dāng)今在高度并發(fā)的連接機(jī)(ConnectionMachine)上，采用Prolog作為軟件語言。僅管由于編譯技術(shù)的改進(jìn)(有了編譯的非解釋型Prolog)，Prolog程序的效率由于依靠參數(shù)束定的合一匹配，它的效率仍不及傳統(tǒng)過程語言。也正是由于它的聲明性質(zhì)，程序員在優(yōu)化算法時(shí)作用有限。因?yàn)樗幕就评硭惴ㄊ谴_定的，且程序正文看不出計(jì)算過程，以不變的遞歸下降算法應(yīng)萬變，當(dāng)然就沒有過程式語言設(shè)計(jì)精巧算法效率高。此外，Prolog的基本推理規(guī)則基于最簡(jiǎn)單的形式邏輯，if_then_else,所以它的功能過程式語言很容易實(shí)現(xiàn)，效率大為提高，只是表達(dá)不如Prolog清晰，所以，近年專家系統(tǒng)的開發(fā)工具不少以C語言實(shí)現(xiàn)，這樣做還利于得到C語言環(huán)境工具的支持。第二個(gè)不足是，一般復(fù)雜的大型系統(tǒng)一開始很難作為證明系統(tǒng)開發(fā)，程序不大運(yùn)算量驚人。而Prolog本身也只有局部量，天生來也不是大型軟件開發(fā)的工具。因此，Prolog只能作為邏輯程序設(shè)計(jì)的獨(dú)枝存在，解決大型應(yīng)用多范型語言是個(gè)出路。12.6小結(jié)?邏輯程序設(shè)計(jì)的基本觀點(diǎn)是程序描述論域上對(duì)象的屬性及其相互關(guān)系，對(duì)象和對(duì)象、對(duì)象和屬性及其相互關(guān)系。對(duì)象和對(duì)象、對(duì)象和屬性的連系就是事實(shí)，事實(shí)之間的關(guān)系以規(guī)則表述。根據(jù)規(guī)則找出合理的事實(shí)叫推理。?謂詞以公式表達(dá)對(duì)象及對(duì)象間的關(guān)系，謂詞公式中的常量、變量、函數(shù)、謂詞、查詢按一定邏輯規(guī)則的變換(等價(jià)置換)即謂詞演算。?子句邏輯是經(jīng)典邏輯的特例，任一謂詞演算公式均可化為’或'連接的子句的集合（子句內(nèi)部由'與'連接）。證明系統(tǒng)是應(yīng)用公理演繹出定理的合法演繹規(guī)則的集合，公理即證明的前題是事實(shí)和規(guī)則的集合。演繹也叫歸約，是證明系統(tǒng)中合法規(guī)則的一次應(yīng)用。演繹的結(jié)果是從前題（公理）導(dǎo)出邏輯結(jié)論。證明是一個(gè)語句序列，證明過程是要么使每個(gè)語句演繹成公理，要么演繹為前此導(dǎo)出的定理，反駁是反向證明一個(gè)語句是矛盾。?一個(gè)語句若能從公理推演出來稱定理，定理集合稱理論。理論不含相互矛盾的定理。理論要借助模型得到語義解釋，模型即特定論域上的約定。一般說來，一個(gè)理論可以有多個(gè)模型。命題演算是謂詞演算的特例。謂詞演算對(duì)于真命題的證明是完整的，但是否能找到證明是不可判定的。不存在，也不可能找到一個(gè)算法驗(yàn)證非真命題。經(jīng)典邏輯從前題到結(jié)論的推理一般采取窮舉證明技術(shù)，在實(shí)現(xiàn)上效率是根本問題，因?yàn)楦鞴斫M合實(shí)現(xiàn)的推理樹往往是天文數(shù)字，即證明系統(tǒng)的組合爆炸問題。基于子句邏輯的歸結(jié)證明技術(shù)以歸結(jié)―合一方法證明反命題恒假來說明命題為真。歸結(jié)原理是將兩個(gè)含有正逆命題的子句消解為更簡(jiǎn)單的歸結(jié)式，如果歸結(jié)得不出矛盾要無休止地歸結(jié)下去直至空間耗盡。反之原命題得證。?對(duì)命題形式進(jìn)一步限制（用Horn子句）和利用切斷技術(shù)（cut操作）是能付諸實(shí)用的超級(jí)歸結(jié)法。它是Prolog的理論模型。邏輯程序設(shè)計(jì)的風(fēng)格不是描述計(jì)算過程而是證明過程。一般構(gòu)造一個(gè)希望的解，證明它就是所希望的解。構(gòu)造過程就實(shí)施了計(jì)算。第二個(gè)特點(diǎn)是描述性。第三個(gè)特點(diǎn)是大量利用表的數(shù)據(jù)結(jié)構(gòu)和遞歸。?Prolog程序公理部分是事實(shí)和規(guī)則（無條件和條件子句），查詢是求證目標(biāo)。它在封閉世界（限于規(guī)則和事實(shí)庫）完成證明的演繹過程。回溯是實(shí)現(xiàn)各子目標(biāo)同時(shí)滿足的唯一方法。?子句邏輯的不可判定性要求規(guī)則和查詢用非反條件，且慎用not操作。?Prolog的優(yōu)點(diǎn)是自文檔性、非過程性、邏輯表達(dá)能力強(qiáng)。描述性使程序清晰、具有潛在的并行性。Prolog的缺點(diǎn)是只適合較小程序。計(jì)算效率不高。習(xí)題試述邏輯程序設(shè)計(jì)的基本風(fēng)格與過程式程序函數(shù)式程序的同異。答：無論是命令式還是函數(shù)式程序都把程序看做是輸入到輸出的某種映射，為了實(shí)現(xiàn)這種映射，程序要對(duì)數(shù)據(jù)結(jié)構(gòu)實(shí)施某個(gè)算法過程，算法實(shí)現(xiàn)該程序功能。而算法又是以程序語言提供的控制機(jī)制實(shí)現(xiàn)計(jì)算邏輯。但這種邏輯是在程序員心里，被隱式體現(xiàn)在程序正文中，為此，程序正確性的證明還要把它隱含的邏輯以斷言形式地寫出來。而邏輯程序設(shè)計(jì)的范型是陳述事實(shí)，制定規(guī)則，程序設(shè)計(jì)就是構(gòu)造證明。程序的執(zhí)行就是在推理。它們的共同之處在于：程序描述的都是數(shù)據(jù)對(duì)象之間的關(guān)系，只是邏輯式程序設(shè)計(jì)抽象層次更高，而不僅限于函數(shù)（映射）關(guān)系。試述歸結(jié)證明的基本思想。為什么要超級(jí)歸結(jié)？答：歸結(jié)法是命題演算中對(duì)合適公式的一種證明方法。其基本思想為：為了證明合適公式F為真，歸結(jié)法證明「F恒假來代替F永真。歸結(jié)原理是：設(shè)有前提LVP和7LVR,則其邏輯結(jié)論是PVR,這個(gè)推理把兩個(gè)子句合并消去一對(duì)正逆命題。將新的子句再加入歸結(jié)子句集中，繼續(xù)歸結(jié)。若最終歸結(jié)式為空則表示此次證明的邏輯結(jié)論是矛盾，原待證結(jié)論若不取反則恒真，命題得證。使用超級(jí)歸結(jié)的原因是：由以上思想可知，如果得不出矛盾，那么歸結(jié)法要無休止地做下去，中間歸結(jié)式也越多，匹配查找次數(shù)越多，每一步都做長(zhǎng)時(shí)間計(jì)算。于是想出比這種原始?xì)w結(jié)更好的辦法，即利用切斷操作，并對(duì)子句形式進(jìn)一步限制即為超級(jí)歸結(jié)法。超級(jí)歸結(jié)實(shí)際上是將無條件Horn子句中的謂詞符號(hào)和條件子句中的對(duì)應(yīng)謂詞符號(hào)合一。何謂變量例化？在演繹過程中變量如何實(shí)例化？何謂命題演算，謂詞演算，它們的同異。12.5謂詞與關(guān)系的同異？答：關(guān)系是泛指事物之間的相互關(guān)系，從邏輯程序設(shè)計(jì)的觀點(diǎn)來看，關(guān)系包括事實(shí)(即對(duì)象和對(duì)象，對(duì)象和屬性的聯(lián)系)及規(guī)則(即事實(shí)之間的關(guān)系)兩種，指數(shù)據(jù)對(duì)象具有的性質(zhì)及不同對(duì)象的聯(lián)系。