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

《第六章逻辑式程序设计语言.ppt》由会员分享，可在线阅读，更多相关《第六章逻辑式程序设计语言.ppt（46页珍藏版）》请在优知文库上搜索。

1、 第六章 逻辑式程序设计语言逻辑式语言基本形式：用一种符号逻辑作为程序设计语言来进行程序设计，通常称为逻辑程序设计语言，或声明性语言第六章 逻辑式程序设计语言程序要对数据结构实施某个算法过程,算法实现计算逻辑 算法 = 逻辑 + 控制逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述，根据规则找出合乎逻辑的事实就是推理逻辑程序设计范型是陈述事实、制定规则，程序设计就是构造证明。程序的执行就在推理6.1谓词演算谓词演算 谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型 表示命题表示命题 表示

2、命题之间的关系表示命题之间的关系 描述如何根据假设为真的命题推断出新命题描述如何根据假设为真的命题推断出新命题 谓词演算诸元素谓词演算诸元素 用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质(properties)， 以及对象间有些什么关系(relations) 描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换，即谓词演算(predicate calculus)(1)公式 由一组约定的符号组成的序列，它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量 指明论域上的对象(3)变量 可束定到特定域上某个范围的对象上(4)函数 表征对象具有的映射关系

3、(5)谓词 表征对象某种性质的符号(6)量词 量词限定的变量名作用域是整个公式(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

4、， changping) True divide (23， 7， 3， N) N未例化， 不知真假谓词的量化量化谓词 结果值 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)

5、 X(a (X) b(X) c (X， g(X)4 消除前束范式的全称量词 a(X) b(X) c (X，g(X) 一般谓词公式变换为子句的实例。一般谓词公式变换为子句的实例。号为号为“可推出可推出”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) 证明系

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

7、的公理一个语句若能从公理出发推演出来，一个语句若能从公理出发推演出来， 则称则称合法语合法语句句， 任何合法语句也叫做任何合法语句也叫做定理定理(theorem)从某一公理集合导出的所有定理集合称为从某一公理集合导出的所有定理集合称为理论理论(theory) 模型模型 从公理集合中导出定理集称之为从公理集合中导出定理集称之为理论理论，有了理论，有了理论我们要解释它的语义必须借助某个我们要解释它的语义必须借助某个模型模型(model)。因因为形式系统只是符号抽象，借助模型我们可为每个常为形式系统只是符号抽象，借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个量、函数、谓词符号找

8、到真理性的解释。即定义每个论域，并表明域上成员和常量公理之间的关系。论域，并表明域上成员和常量公理之间的关系。 公理的谓词符号必须派定为域中对象的性质，公理的谓词符号必须派定为域中对象的性质， 函数派定为对域中对象的操作。函数派定为对域中对象的操作。 公理集合一般情况下只是定义的部分公理集合一般情况下只是定义的部分(偏偏)函数和函数和谓词，谓词， 是问题域的一个侧面。是问题域的一个侧面。 所以能满足该理论的所以能满足该理论的模型往往不止一个。模型往往不止一个。例例 一个最简单的理论一个最简单的理论 公理集公理集: Xinterval(X)not interval (X+1) (a1) Xnot

9、 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)，也不能证明，也不能证明not interval(3)为为真命题。这就是真命题。这就是Hilbert讨论过的讨论过的可判定可判定(decidability)问题。

10、问题。 1936年年Church和和Turing证实谓词演算可判定性问题是没有解的证实谓词演算可判定性问题是没有解的 一旦我们断言一旦我们断言interval(3)或或interval(2)是真命题是真命题,我们立刻可通过我们立刻可通过演绎证明按这个理论写出的每一个谓词为真。这就是演绎证明按这个理论写出的每一个谓词为真。这就是Godel和和Herbrand1930年证实的谓词演算具备的完整性年证实的谓词演算具备的完整性(completeness) 证明技术证明技术 从谓词演算具有完整性，从谓词演算具有完整性， 理论上可证明按公理理论上可证明按公理集合建立的任何理论。关键是效率。集合建立的任何理

11、论。关键是效率。 如果我们从公理出发做出每一个步骤，如果我们从公理出发做出每一个步骤， 在新的在新的步骤上仍然要查找每一个公理，找出可能的推理。步骤上仍然要查找每一个公理，找出可能的推理。如此下去就形成一个庞大的树行公理集，如此下去就形成一个庞大的树行公理集， 每层的结每层的结点表示一个公理的语句，点表示一个公理的语句， 其深度和宽度随问题和最其深度和宽度随问题和最初给出的公理而定，初给出的公理而定， 一层一步骤，一层一步骤， N层的树就是层的树就是N步推理。步推理。 对于自动定理证明程序，对于自动定理证明程序， 只有穷举每条可能的证只有穷举每条可能的证明步骤才能说它是完全的。明步骤才能说它是

12、完全的。 穷举完所有路径马上遇穷举完所有路径马上遇到组合爆炸问题，无论是深度优先还是广度优先，到组合爆炸问题，无论是深度优先还是广度优先，百步演绎可能的路径数都是天文数字。百步演绎可能的路径数都是天文数字。 归结定理证明归结定理证明 J.A.Robinson1965年提出的年提出的归结法归结法(resolution) ，是，是命题演算中对合适公式的一种证明方法。命题演算中对合适公式的一种证明方法。 为了证明合适公式为了证明合适公式F为真，为真， 归结法证明归结法证明 F恒假来代恒假来代替替F永真。永真。 把两子句合一把两子句合一(unification)并消去一对正逆命题，故并消去一对正逆命题

13、，故归结也译作归结也译作消解消解。 归结证明的过程并称之归结演绎，归结证明的过程并称之归结演绎， 其步骤如下其步骤如下:1把前题中所有命题换成子句形式。把前题中所有命题换成子句形式。2取结论的反取结论的反,并转换成子句形式并转换成子句形式,加入加入1中的子句集中的子句集.3在子句集中选择含有互逆命题的命题归结。用合在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句一算法得出新子句(归结式归结式)，再加入到子句集。，再加入到子句集。4重复重复3，若归结式为空则表示此次证明的逻辑结，若归结式为空则表示此次证明的逻辑结论是矛盾，原待证结论若不取反则恒真。命题得证。论是矛盾，原待证结论若不取反

14、则恒真。命题得证。 否则继续重复否则继续重复3。 例：归结证明例：归结证明 若有前题若有前题 待证命题待证命题 取反得新子句取反得新子句 p1 Q P P U p5 P p2 R Q p6 U p3 S R p4 U S 取待证命题的反，取待证命题的反， 得得PU， 它是它是连接的两个子句连接的两个子句P、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)操作，操作， 并利用对子句形式进并利用对子句形式进一步限制的一步限制的超级归结法超级归结法(

16、Hyperresolution)。 Horn子句实现超归结子句实现超归结 Horn子句是至多只有一个非负谓词符号的子句子句是至多只有一个非负谓词符号的子句 Horn子句形式示例如下子句形式示例如下: P QS R T 其中只有一个非负谓词其中只有一个非负谓词S,可作以下演算：可作以下演算： 先将先将S移向右方移向右方 S P Q 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(new_list) sorted(list) j