第六章邏輯式程序設(shè)計語言

《第六章邏輯式程序設(shè)計語言》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在教育資源-天天文庫。

1、第六章邏輯式程序設(shè)計語言程序要對數(shù)據(jù)結(jié)構(gòu)實施某個算法過程,算法實現(xiàn)計算邏輯算法=邏輯+控制邏輯程序設(shè)計的基本觀點是程序描述的是數(shù)據(jù)對象之間的關(guān)系。關(guān)系也是聯(lián)系對象和對象、對象和屬性的聯(lián)系就是我們所說的事實。事實之間的關(guān)系以規(guī)則表述，根據(jù)規(guī)則找出合乎邏輯的事實就是推理邏輯程序設(shè)計范型是陳述事實、制定規(guī)則，程序設(shè)計就是構(gòu)造證明。程序的執(zhí)行就在推理6.1謂詞演算謂詞演算是符號化事實的形式邏輯系統(tǒng)，它也是邏輯程序設(shè)計語言的模型謂詞演算諸元素用形式方法研究論域上的對象需要一種語言，它能表達(dá)該域?qū)ο缶哂惺裁葱再|(zhì)(properties)，以及對象間有些什么

2、關(guān)系(relations)描述以公式(Formulas)表達(dá)。謂詞公式中各元素按一定邏輯規(guī)則變換，即謂詞演算(predicatecalculus)(1)公式由一組約定的符號組成的序列，它包括常量、變量、邏輯連接、命題函數(shù)、謂詞、量詞(2)常量指明論域上的對象(3)變量可束定到特定域上某個范圍的對象上(4)函數(shù)表征對象具有的映射關(guān)系(5)謂詞表征對象某種性質(zhì)的符號(6)量詞量詞限定的變量名作用域是整個公式(7)邏輯操作and，or，not，→(蘊含)<＝>(全等)當(dāng)謂詞應(yīng)用到的變元是常量或已被束定的變量上時，就叫做句子(sentence)或命題

3、(proposition)謂詞變元的個數(shù)稱作目(arity)，有單目、N目謂詞之稱N-目謂詞的例子。謂詞目含義odd(X)1X是奇數(shù)father(F，S)2F是S的父親divide(N，D，Q，R)4N除D得商Q和余數(shù)R謂詞例化結(jié)果值odd(2)Falsedivide(23，7，3，2)Turefather(changshan，changping)Truedivide(23，7，3，N)N未例化，不知真假謂詞的量化量化謂詞結(jié)果值?Xodd(X)False?Xodd(X)True?X(X=2*Y+1→odd(X))True?X?Ydivide(

4、X，3，Y，0)False?X?Ydivide(X，3，Y，0)True，如X=3，Y=1?X?Ydivide(X，3，Y，0)False，但很難證明證明一個全稱謂詞是比較難的，因為最可靠的證明方法是枚舉例證。于是采取反證的方法，全稱量化的謂詞取反量化謂詞取反?Xodd(X)?Xnotodd(X)[1]?Xodd(X)?Xnotodd(X)[2]?X(X=2*Y+1→odd(X))?Xnot(X+2*Y+1→odd(X))[3]?Xnot(X=2*Y+1)orodd(X))[4]?X((X=2*Y+1)andnotadd(X))[5]?X?Y

5、divide(X，3，Y，0)?X?Ynotdivide(X，3，Y，0)[6]?X?Ydivide(X，3，Y，0)?X?Ynotdivide(X，3，Y，0)[7]?X?Ydivide(X，3，Y，0)?X?Ynotdivide(X，3，Y，0)[8]謂詞演算的等價變換[1]以∧，∨，?消除→、<=>符號[2]化為前束范式,消除最外的?符號,否定符號內(nèi)移?(?XP(X)┠?X(?p(X))[3]用斯柯林變換消去存在量詞?X(a(X)∧b(X)∨?Yc(X，Y))┠?X(a(X)∧b(X)∨c(X，g(X)))[4]消除前束范式的全稱量詞┠

6、a(X)∧b(X)∨c(X，g(X))一般謂詞公式變換為子句的實例?！摹枮椤翱赏瞥觥盵5]用分配率P∨(Q∧R)=(P∨Q)∧(P∨R)化成合取范式┠(a(X)∨c(X，g(X)))∧(b(X)∨c(X，g(X)))經(jīng)過以上變換,任何一復(fù)合公式均可成為如下形式:F=C1∧C2∧…Cn且其中Ci稱為子句若以';'代'∨'則有:Ci=L1∨L2∨…Lv=L1;L2;…;Lv因此，任一公式均可化為'∨'連接的子句的集合6.2自動定理證明證明系統(tǒng)事實即證明系統(tǒng)中的公理(axioms)證明系統(tǒng)(proofsystem)是應(yīng)用公理演繹出定理(theo

7、rems)的合法演繹規(guī)則的集合演繹也叫歸約(deduction)，是對證明系統(tǒng)中合法推理規(guī)則的一次應(yīng)用演繹從公理導(dǎo)出結(jié)論(conclusion)，中間可利用以這些規(guī)則演繹出的定理證明(proof)是個語句序列，以每個語句得到證明而結(jié)束，即每個句子要么演繹成公理，要么演繹成前此導(dǎo)出的定理一個證明若有N個語句(命題)則稱N步證明反駁(refutation)是一個語句的反向證明。它證明一個語句是矛盾的，即不合乎給定的公理一個語句若能從公理出發(fā)推演出來，則稱合法語句，任何合法語句也叫做定理(theorem)從某一公理集合導(dǎo)出的所有定理集合稱為理論(t

8、heory)模型從公理集合中導(dǎo)出定理集稱之為理論，有了理論我們要解釋它的語義必須借助某個模型(model)。因為形式系統(tǒng)只是符號抽象，借助模型我們可為每個常量、函數(shù)