第六章逻辑式程序设计语言课件.ppt
- 【下载声明】
1. 本站全部试题类文档,若标题没写含答案,则无答案;标题注明含答案的文档,主观题也可能无答案。请谨慎下单,一旦售出,不予退换。
2. 本站全部PPT文档均不含视频和音频,PPT中出现的音频或视频标识(或文字)仅表示流程,实际无音频或视频文件。请谨慎下单,一旦售出,不予退换。
3. 本页资料《第六章逻辑式程序设计语言课件.ppt》由用户(晟晟文业)主动上传,其收益全归该用户。163文库仅提供信息存储空间,仅对该用户上传内容的表现方式做保护处理,对上传内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知163文库(点击联系客服),我们立即给予删除!
4. 请根据预览情况,自愿下载本文。本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
5. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007及以上版本和PDF阅读器,压缩文件请下载最新的WinRAR软件解压。
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 第六 逻辑 程序设计语言 课件
- 资源描述:
-
1、 第六章 逻辑式程序设计语言逻辑式语言基本形式:用一种符号逻辑作为程序设计语言来进行程序设计,通常称为逻辑程序设计语言,或声明性语言第六章 逻辑式程序设计语言程序要对数据结构实施某个算法过程,算法实现计算逻辑 算法=逻辑+控制逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述,根据规则找出合乎逻辑的事实就是推理逻辑程序设计范型是陈述事实、制定规则,程序设计就是构造证明。程序的执行就在推理6.1谓词演算谓词演算 谓词演算是符号化事实的形式逻辑系统,它也是逻辑程序设计语言的模型 表示命题 表示命题之间的关系
2、描述如何根据假设为真的命题推断出新命题 谓词演算诸元素谓词演算诸元素 用形式方法研究论域上的对象需要一种语言,它能表达该域对象具有什么性质(properties),以及对象间有些什么关系(relations)描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换,即谓词演算(predicate calculus)(1)公式 由一组约定的符号组成的序列,它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量 指明论域上的对象(3)变量 可束定到特定域上某个范围的对象上(4)函数 表征对象具有的映射关系(5)谓词 表征对象某种性质的符号(6)量词 量词限定的变量名作用域是整个公
3、式(7)逻辑操作 and,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未例化,不知真假谓词的量化量化谓词 结果
4、值 Xodd(X)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、为“可推出可推出”5用分配率P(QR)=(PQ)(PR)化成合取范式 (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),是对证明系统中合法 推理规则的一次应用 演绎从公理导出结论(conclu
6、sion),中间可利用以 这些规则演绎出的定理证明证明(proof)是个语句序列,以每个语句得到证明而结束,即每个句子要么演绎成公理,要么演绎成前此导出的定理一个证明若有一个证明若有N个语句个语句(命题命题)则称则称N步证明步证明反驳反驳(refutation)是一个语句的反向证明。是一个语句的反向证明。它证明它证明 一个语句是矛盾的,一个语句是矛盾的,即不合乎给定的公理即不合乎给定的公理一个语句若能从公理出发推演出来,一个语句若能从公理出发推演出来,则称则称合法语合法语句句,任何合法语句也叫做任何合法语句也叫做定理定理(theorem)从某一公理集合导出的所有定理集合称为从某一公理集合导出的
7、所有定理集合称为理论理论(theory)模型模型 从公理集合中导出定理集称之为从公理集合中导出定理集称之为理论理论,有了理论,有了理论我们要解释它的语义必须借助某个我们要解释它的语义必须借助某个模型模型(model)。因因为形式系统只是符号抽象,借助模型我们可为每个常为形式系统只是符号抽象,借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个量、函数、谓词符号找到真理性的解释。即定义每个论域,并表明域上成员和常量公理之间的关系。论域,并表明域上成员和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质,公理的谓词符号必须派定为域中对象的性质,函数派定为对域中对象的操作。函
8、数派定为对域中对象的操作。公理集合一般情况下只是定义的部分公理集合一般情况下只是定义的部分(偏偏)函数和函数和谓词,谓词,是问题域的一个侧面。是问题域的一个侧面。所以能满足该理论的所以能满足该理论的模型往往不止一个。模型往往不止一个。例例 一个最简单的理论一个最简单的理论 公理集公理集: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
9、)谓词谓词interval(间隔数间隔数)在整数域上有两个子域在整数域上有两个子域odd、even都能够满都能够满足间隔数理论不能证明足间隔数理论不能证明interval(3),也不能证明,也不能证明not interval(3)为为真命题。这就是真命题。这就是Hilbert讨论过的讨论过的可判定可判定(decidability)问题。问题。1936年年Church和和Turing证实谓词演算可判定性问题是没有解的证实谓词演算可判定性问题是没有解的 一旦我们断言一旦我们断言interval(3)或或interval(2)是真命题是真命题,我们立刻可通过我们立刻可通过演绎证明按这个理论写出的每一
10、个谓词为真。这就是演绎证明按这个理论写出的每一个谓词为真。这就是Godel和和Herbrand1930年证实的谓词演算具备的完整性年证实的谓词演算具备的完整性(completeness)证明技术证明技术 从谓词演算具有完整性,从谓词演算具有完整性,理论上可证明按公理理论上可证明按公理集合建立的任何理论。关键是效率。集合建立的任何理论。关键是效率。如果我们从公理出发做出每一个步骤,如果我们从公理出发做出每一个步骤,在新的在新的步骤上仍然要查找每一个公理,找出可能的推理。步骤上仍然要查找每一个公理,找出可能的推理。如此下去就形成一个庞大的树行公理集,如此下去就形成一个庞大的树行公理集,每层的结每层
11、的结点表示一个公理的语句,点表示一个公理的语句,其深度和宽度随问题和最其深度和宽度随问题和最初给出的公理而定,初给出的公理而定,一层一步骤,一层一步骤,N层的树就是层的树就是N步推理。步推理。对于自动定理证明程序,对于自动定理证明程序,只有穷举每条可能的证只有穷举每条可能的证明步骤才能说它是完全的。明步骤才能说它是完全的。穷举完所有路径马上遇穷举完所有路径马上遇到组合爆炸问题,无论是深度优先还是广度优先,到组合爆炸问题,无论是深度优先还是广度优先,百步演绎可能的路径数都是天文数字。百步演绎可能的路径数都是天文数字。归结定理证明归结定理证明 J.A.Robinson1965年提出的年提出的归结法
12、归结法(resolution),是,是命题演算中对合适公式的一种证明方法。命题演算中对合适公式的一种证明方法。为了证明合适公式为了证明合适公式F为真,为真,归结法证明归结法证明 F恒假来代恒假来代替替F永真。永真。把两子句合一把两子句合一(unification)并消去一对正逆命题,故并消去一对正逆命题,故归结也译作归结也译作消解消解。归结证明的过程并称之归结演绎,归结证明的过程并称之归结演绎,其步骤如下其步骤如下:1把前题中所有命题换成子句形式。把前题中所有命题换成子句形式。2取结论的反取结论的反,并转换成子句形式并转换成子句形式,加入加入1中的子句集中的子句集.3在子句集中选择含有互逆命题
13、的命题归结。用合在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句一算法得出新子句(归结式归结式),再加入到子句集。,再加入到子句集。4重复重复3,若归结式为空则表示此次证明的逻辑结,若归结式为空则表示此次证明的逻辑结论是矛盾,原待证结论若不取反则恒真。命题得证。论是矛盾,原待证结论若不取反则恒真。命题得证。否则继续重复否则继续重复3。例:归结证明例:归结证明 若有前题若有前题 待证命题待证命题 取反得新子句取反得新子句 p1 Q P P U p5 P p2 R Q p6 U p3 S R p4 U S 取待证命题的反,取待证命题的反,得得PU,它是它是连接的两个子句连接的两个子句P、
14、U,把它们加到前题子句集,把它们加到前题子句集,为为p5,p6。归结演绎如下图归结演绎如下图:Q P P p1-p5归结归结 Q R Q 再与再与p2归结归结 S R R 再与再与p3归结归结 S U S 再与再与p4归结归结 U U 再与再与p6归结归结 矛盾矛盾由本例可以看出两个问题:由本例可以看出两个问题:第一,归结法是由合一算法实现的。所谓第一,归结法是由合一算法实现的。所谓合一合一是找出是找出型式匹配的两子句,型式匹配的两子句,将它们合一为归结式,将它们合一为归结式,相当于相当于代数中的化简。代数中的化简。第二,如果得不出矛盾,那么归结法要无休止地做下第二,如果得不出矛盾,那么归结法
15、要无休止地做下去,中间归结式出得越多,去,中间归结式出得越多,匹配查找次数越多,匹配查找次数越多,每每一步都做长时间计算。一步都做长时间计算。Solution:利用切断利用切断(cut)操作,操作,并利用对子句形式进并利用对子句形式进一步限制的一步限制的超级归结法超级归结法(Hyperresolution)。Horn子句实现超归结子句实现超归结 Horn子句是至多只有一个非负谓词符号的子句子句是至多只有一个非负谓词符号的子句 Horn子句形式示例如下子句形式示例如下:P QS R T 其中只有一个非负谓词其中只有一个非负谓词S,可作以下演算:可作以下演算:先将先将S移向右方移向右方 S P Q
16、 R T 按德按德摩根定律摩根定律 S (PQRT)即即,则则 S(P Q R T)此条件此条件Horn子句的意义是子句的意义是 if S then(PQRT)。若若S为空,为空,则为无条件则为无条件Horn子句,子句,是一个断言是一个断言(事实事实)6.3 逻辑程序的风格逻辑程序的风格第一第一个特点是它不描述计算过程而是描述证明过程个特点是它不描述计算过程而是描述证明过程第二个特点是描述性第二个特点是描述性第三个特点是大量用表和递归实现重复操作第三个特点是大量用表和递归实现重复操作sort(old_list,new_list)permute(old_list,new_list)sorted(
17、new_list)sorted(list)j 使得 1 j n,list(j)list(j+1)*permute是一个谓词,如果第二个参数组是第一个参数组的一个排列,就返回真Prolog语言 Prolog是一种基于一阶谓词的逻辑式语言 Prolog是基于Horn子句的,使用归结推理,具有很强的逻辑描述能力和推理能力 Prolog语言特点:一阶逻辑的语言形式是形式化地严格定义的 一阶逻辑的语法简易易懂 逻辑公式不需要重复表达,与不同应用无关 事实、假设、推理、查询、视图和完整性规约条件都能以基于一阶逻辑的prolog语言表达 逻辑语言Prolog可作为定义和比较其它知识表示模型的共同模型例例 求
展开阅读全文