資源描述：
《第六章邏輯式程序設(shè)計(jì)語(yǔ)言》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在教育資源-天天文庫(kù)。
1、第六章邏輯式程序設(shè)計(jì)語(yǔ)言程序要對(duì)數(shù)據(jù)結(jié)構(gòu)實(shí)施某個(gè)算法過(guò)程,算法實(shí)現(xiàn)計(jì)算邏輯算法=邏輯+控制邏輯程序設(shè)計(jì)的基本觀點(diǎn)是程序描述的是數(shù)據(jù)對(duì)象之間的關(guān)系。關(guān)系也是聯(lián)系對(duì)象和對(duì)象、對(duì)象和屬性的聯(lián)系就是我們所說(shuō)的事實(shí)。事實(shí)之間的關(guān)系以規(guī)則表述，根據(jù)規(guī)則找出合乎邏輯的事實(shí)就是推理邏輯程序設(shè)計(jì)范型是陳述事實(shí)、制定規(guī)則，程序設(shè)計(jì)就是構(gòu)造證明。程序的執(zhí)行就在推理6.1謂詞演算謂詞演算是符號(hào)化事實(shí)的形式邏輯系統(tǒng)，它也是邏輯程序設(shè)計(jì)語(yǔ)言的模型謂詞演算諸元素用形式方法研究論域上的對(duì)象需要一種語(yǔ)言，它能表達(dá)該域?qū)ο缶哂惺裁葱再|(zhì)(properties)，以及對(duì)象間有些什么
2、關(guān)系(relations)描述以公式(Formulas)表達(dá)。謂詞公式中各元素按一定邏輯規(guī)則變換，即謂詞演算(predicatecalculus)(1)公式由一組約定的符號(hào)組成的序列，它包括常量、變量、邏輯連接、命題函數(shù)、謂詞、量詞(2)常量指明論域上的對(duì)象(3)變量可束定到特定域上某個(gè)范圍的對(duì)象上(4)函數(shù)表征對(duì)象具有的映射關(guān)系(5)謂詞表征對(duì)象某種性質(zhì)的符號(hào)(6)量詞量詞限定的變量名作用域是整個(gè)公式(7)邏輯操作and，or，not，→(蘊(yùn)含)<＝>(全等)當(dāng)謂詞應(yīng)用到的變?cè)浅Ａ炕蛞驯皇ǖ淖兞可蠒r(shí)，就叫做句子(sentence)或命題
3、(proposition)謂詞變?cè)膫€(gè)數(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，但很難證明證明一個(gè)全稱謂詞是比較難的，因?yàn)樽羁煽康淖C明方法是枚舉例證。于是采取反證的方法，全稱量化的謂詞取反量化謂詞取反?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]謂詞演算的等價(jià)變換[1]以∧，∨，?消除→、<=>符號(hào)[2]化為前束范式,消除最外的?符號(hào),否定符號(hào)內(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))一般謂詞公式變換為子句的實(shí)例?！摹?hào)為“可推出”[5]用分配率P∨(Q∧R)=(P∨Q)∧(P∨R)化成合取范式┠(a(X)∨c(X，g(X)))∧(b(X)∨c(X，g(X)))經(jīng)過(guò)以上變換,任何一復(fù)合公式均可成為如下形式:F=C1∧C2∧…Cn且其中Ci稱為子句若以';'代'∨'則有:Ci=L1∨L2∨…Lv=L1;L2;…;Lv因此，任一公式均可化為'∨'連接的子句的集合6.2自動(dòng)定理證明證明系統(tǒng)事實(shí)即證明系統(tǒng)中的公理(axioms)證明系統(tǒng)(proofsystem)是應(yīng)用公理演繹出定理(theo
7、rems)的合法演繹規(guī)則的集合演繹也叫歸約(deduction)，是對(duì)證明系統(tǒng)中合法推理規(guī)則的一次應(yīng)用演繹從公理導(dǎo)出結(jié)論(conclusion)，中間可利用以這些規(guī)則演繹出的定理證明(proof)是個(gè)語(yǔ)句序列，以每個(gè)語(yǔ)句得到證明而結(jié)束，即每個(gè)句子要么演繹成公理，要么演繹成前此導(dǎo)出的定理一個(gè)證明若有N個(gè)語(yǔ)句(命題)則稱N步證明反駁(refutation)是一個(gè)語(yǔ)句的反向證明。它證明一個(gè)語(yǔ)句是矛盾的，即不合乎給定的公理一個(gè)語(yǔ)句若能從公理出發(fā)推演出來(lái)，則稱合法語(yǔ)句，任何合法語(yǔ)句也叫做定理(theorem)從某一公理集合導(dǎo)出的所有定理集合稱為理論(t
8、heory)模型從公理集合中導(dǎo)出定理集稱之為理論，有了理論我們要解釋它的語(yǔ)義必須借助某個(gè)模型(model)。因?yàn)樾问较到y(tǒng)只是符號(hào)抽象，借助模型我們可為每個(gè)常量、函數(shù)
