第六章逻辑式程序设计语言

《第六章逻辑式程序设计语言》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第六章逻辑式程序设计语言程序要对数据结构实施某个算法过程,算法实现计算逻辑算法=逻辑+控制逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述，根据规则找出合乎逻辑的事实就是推理逻辑程序设计范型是陈述事实、制定规则，程序设计就是构造证明。程序的执行就在推理6.1谓词演算谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型谓词演算诸元素用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质(properties)，以及对象间有些什么

2、关系(relations)描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换，即谓词演算(predicatecalculus)(1)公式由一组约定的符号组成的序列，它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量指明论域上的对象(3)变量可束定到特定域上某个范围的对象上(4)函数表征对象具有的映射关系(5)谓词表征对象某种性质的符号(6)量词量词限定的变量名作用域是整个公式(7)逻辑操作and，or，not，→(蕴含)<＝>(全等)当谓词应用到的变元是常量或已被束定的变量上时，就叫做句子(sentence)或命题

3、(proposition)谓词变元的个数称作目(arity)，有单目、N目谓词之称N-目谓词的例子。谓词目含义odd(X)1X是奇数father(F，S)2F是S的父亲divide(N，D，Q，R)4N除D得商Q和余数R谓词例化结果值odd(2)Falsedivide(23，7，3，2)Turefather(changshan，changping)Truedivide(23，7，3，N)N未例化，不知真假谓词的量化量化谓词结果值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]化为前束范式,消除最外的符号,否定符号内移(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)))经过以上变换,任何一复合公式均可成为如下形式:F=C1∧C2∧…Cn且其中Ci称为子句若以';'代'∨'则有:Ci=L1∨L2∨…Lv=L1;L2;…;Lv因此，任一公式均可化为'∨'连接的子句的集合6.2自动定理证明证明系统事实即证明系统中的公理(axioms)证明系统(proofsystem)是应用公理演绎出定理(theo

7、rems)的合法演绎规则的集合演绎也叫归约(deduction)，是对证明系统中合法推理规则的一次应用演绎从公理导出结论(conclusion)，中间可利用以这些规则演绎出的定理证明(proof)是个语句序列，以每个语句得到证明而结束，即每个句子要么演绎成公理，要么演绎成前此导出的定理一个证明若有N个语句(命题)则称N步证明反驳(refutation)是一个语句的反向证明。它证明一个语句是矛盾的，即不合乎给定的公理一个语句若能从公理出发推演出来，则称合法语句，任何合法语句也叫做定理(theorem)从某一公理集合导出的所有定理集合称为理论(t

8、heory)模型从公理集合中导出定理集称之为理论，有了理论我们要解释它的语义必须借助某个模型(model)。因为形式系统只是符号抽象，借助模型我们可为每个常量、函数