第六章逻辑式程序设计语言.ppt
《第六章逻辑式程序设计语言.ppt》由会员分享,可在线阅读,更多相关《第六章逻辑式程序设计语言.ppt(46页珍藏版)》请在课桌文档上搜索。
1、第六章 逻辑式程序设计语言,逻辑式语言基本形式:用一种符号逻辑作为程序设计语言来进行程序设计,通常称为逻辑程序设计语言,或声明性语言,第六章 逻辑式程序设计语言,程序要对数据结构实施某个算法过程,算法实现计算逻辑 算法=逻辑+控制逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述,根据规则找出合乎逻辑的事实就是推理逻辑程序设计范型是陈述事实、制定规则,程序设计就是构造证明。程序的执行就在推理,6.1谓词演算,谓词演算是符号化事实的形式逻辑系统,它也是逻辑程序设计语言的模型表示命题表示命题之间的关系描述如何
2、根据假设为真的命题推断出新命题 谓词演算诸元素 用形式方法研究论域上的对象需要一种语言,它能表达该域对象具有什么性质(properties),以及对象间有些什么关系(relations)描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换,即谓词演算(predicate calculus),(1)公式 由一组约定的符号组成的序列,它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量 指明论域上的对象(3)变量 可束定到特定域上某个范围的对象上(4)函数 表征对象具有的映射关系(5)谓词 表征对象某种性质的符号(6)量词 量词限定的变量名作用域是整个公式(7)逻辑操作 a
3、nd,or,not,(蕴含)(全等)当谓词应用到的变元是常量或已被束定的变量上时,就叫做句子(sentence)或命题(proposition),谓词变元的个数称作目(arity),有单目、N目谓词之称 N-目谓词的例子。谓词 目 含义 odd(X)1 X是奇数 father(F,S)2 F是S的父亲 divide(N,D,Q,R)4 N除D得商Q和余数R 谓词例化 结果值 odd(2)False divide(23,7,3,2)Ture father(changshan,changping)True divide(23,7,3,N)N未例化,不知真假,谓词的量化量化谓词 结果值 Xodd(X
4、)False Xodd(X)True X(X=2*Y+1odd(X)True XYdivide(X,3,Y,0)True,如X=3,Y=1XYdivide(X,3,Y,0)FalseXYdivide(X,3,Y,0)False,但很难证明,谓词演算的等价变换,1以,消除、符号2化为前束范式,消除最外的符号,否定符号内移(XP(X)X(p(X)3用斯柯林变换消去存在量词 X(a(X)b(X)Y c(X,Y)X(a(X)b(X)c(X,g(X)4 消除前束范式的全称量词 a(X)b(X)c(X,g(X),一般谓词公式变换为子句的实例。号为“可推出”,5用分配率P(QR)=(PQ)(PR)化成合取范
5、式(a(X)c(X,g(X)(b(X)c(X,g(X)经过以上变换,任何一复合公式均可成为如下形式:F=C1C2 Cn 且其中Ci称为子句 若以;代则有:Ci=L1 L2 Lv=L1;L2;Lv 因此,任一公式均可化为连接的子句的集合,6.2 自动定理证明,证明系统 事实即证明系统中的公理(axioms)证明系统(proof system)是应用公理演绎出定理(theorems)的合法演绎规则的集合 演绎也叫归约(deduction),是对证明系统中合法 推理规则的一次应用 演绎从公理导出结论(conclusion),中间可利用以 这些规则演绎出的定理证明(proof)是个语句序列,以每个语句
6、得到证明而结束,即每个句子要么演绎成公理,要么演绎成前此导出的定理,一个证明若有N个语句(命题)则称N步证明反驳(refutation)是一个语句的反向证明。它证明 一个语句是矛盾的,即不合乎给定的公理一个语句若能从公理出发推演出来,则称合法语句,任何合法语句也叫做定理(theorem)从某一公理集合导出的所有定理集合称为理论(theory),模型 从公理集合中导出定理集称之为理论,有了理论我们要解释它的语义必须借助某个模型(model)。因为形式系统只是符号抽象,借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个论域,并表明域上成员和常量公理之间的关系。公理的谓词符号必须派
7、定为域中对象的性质,函数派定为对域中对象的操作。公理集合一般情况下只是定义的部分(偏)函数和谓词,是问题域的一个侧面。所以能满足该理论的模型往往不止一个。,例 一个最简单的理论 公理集:Xinterval(X)not interval(X+1)(a1)Xnot interval(X+1)interval(X)(a2)2=1+1(a3)从间隔数公理可导出定理:Xinterval(X)interval(X+2)(t1)Xinterval(X+2)interval(X)(t2),谓词interval(间隔数)在整数域上有两个子域odd、even都能够满足间隔数理论不能证明interval(3),也不
8、能证明not interval(3)为真命题。这就是Hilbert讨论过的可判定(decidability)问题。1936年Church和Turing证实谓词演算可判定性问题是没有解的一旦我们断言interval(3)或interval(2)是真命题,我们立刻可通过演绎证明按这个理论写出的每一个谓词为真。这就是Godel和Herbrand1930年证实的谓词演算具备的完整性(completeness),证明技术 从谓词演算具有完整性,理论上可证明按公理集合建立的任何理论。关键是效率。如果我们从公理出发做出每一个步骤,在新的步骤上仍然要查找每一个公理,找出可能的推理。如此下去就形成一个庞大的树行
9、公理集,每层的结点表示一个公理的语句,其深度和宽度随问题和最初给出的公理而定,一层一步骤,N层的树就是N步推理。对于自动定理证明程序,只有穷举每条可能的证明步骤才能说它是完全的。穷举完所有路径马上遇到组合爆炸问题,无论是深度优先还是广度优先,百步演绎可能的路径数都是天文数字。,归结定理证明 J.A.Robinson1965年提出的归结法(resolution),是命题演算中对合适公式的一种证明方法。为了证明合适公式F为真,归结法证明F恒假来代替F永真。把两子句合一(unification)并消去一对正逆命题,故归结也译作消解。归结证明的过程并称之归结演绎,其步骤如下:,1把前题中所有命题换成子
10、句形式。2取结论的反,并转换成子句形式,加入1中的子句集.3在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句(归结式),再加入到子句集。4重复3,若归结式为空则表示此次证明的逻辑结论是矛盾,原待证结论若不取反则恒真。命题得证。否则继续重复3。,例:归结证明 若有前题 待证命题 取反得新子句 p1 QP PU p5 P p2 RQ p6 U p3 SR p4 US 取待证命题的反,得PU,它是连接的两个子句P、U,把它们加到前题子句集,为p5,p6。,归结演绎如下图:QP P p1-p5归结 Q RQ 再与p2归结 SR R 再与p3归结 S US 再与p4归结 U U 再与p6归结
11、矛盾,由本例可以看出两个问题:第一,归结法是由合一算法实现的。所谓合一是找出型式匹配的两子句,将它们合一为归结式,相当于代数中的化简。第二,如果得不出矛盾,那么归结法要无休止地做下去,中间归结式出得越多,匹配查找次数越多,每一步都做长时间计算。Solution:利用切断(cut)操作,并利用对子句形式进一步限制的超级归结法(Hyperresolution)。,Horn子句实现超归结 Horn子句是至多只有一个非负谓词符号的子句 Horn子句形式示例如下:PQSRT 其中只有一个非负谓词S,可作以下演算:先将S移向右方 SPQRT 按德摩根定律 S(PQRT)即,则 S(P Q R T)此条件H
12、orn子句的意义是 if S then(PQRT)。若S为空,则为无条件Horn子句,是一个断言(事实),6.3 逻辑程序的风格,第一个特点是它不描述计算过程而是描述证明过程第二个特点是描述性第三个特点是大量用表和递归实现重复操作sort(old_list,new_list)permute(old_list,new_list)sorted(new_list)sorted(list)j 使得 1 j n,list(j)list(j+1)*permute是一个谓词,如果第二个参数组是第一个参数组的一个排列,就返回真,Prolog语言,Prolog是一种基于一阶谓词的逻辑式语言Prolog是基于Ho
13、rn子句的,使用归结推理,具有很强的逻辑描述能力和推理能力Prolog语言特点:一阶逻辑的语言形式是形式化地严格定义的一阶逻辑的语法简易易懂逻辑公式不需要重复表达,与不同应用无关事实、假设、推理、查询、视图和完整性规约条件都能以基于一阶逻辑的prolog语言表达逻辑语言Prolog可作为定义和比较其它知识表示模型的共同模型,例 求平均成绩的逻辑程序,打开一分数文件scores,读入分数求和并用的数N除之得平均成绩 average:-see(scores),getinput(Sum,N),seen(scores),Av is Sum/N,print(Average=,Av)getinput(Su
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 第六 逻辑 程序设计语言

链接地址:https://www.desk33.com/p-259745.html