逻辑式程序设计语言.ppt
《逻辑式程序设计语言.ppt》由会员分享,可在线阅读,更多相关《逻辑式程序设计语言.ppt(37页珍藏版)》请在三一文库上搜索。
1、第06章 逻辑式程序设计语言,程序要对数据结构实施某个算法过程,算法实现计算逻辑 算法 = 逻辑 + 控制 逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系 对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述,根据规则找出合乎逻辑的事实就是推理 逻辑程序设计范型是陈述事实、制定规则,程序设计就是构造证明。程序的执行就在推理,6.1谓词演算,谓词演算是符号化事实的形式逻辑系统,它也是逻辑程序设计语言的模型 谓词演算诸元素 用形式方法研究论域上的对象需要一种语言,它能表达该域对象具有什么性质(properties), 以及对象间有些什么关系(relatio
2、ns) 描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换,即谓词演算(predicate calculus),(1)公式 由一组约定的符号组成的序列,它包括常量、变量、逻辑连接、命题函数、谓词、量词 (2)常量 指明论域上的对象 (3)变量 可束定到特定域上某个范围的对象上 (4)函数 表征对象具有的映射关系 (5)谓词 表征对象某种性质的符号 (6)量词 量词限定的变量名作用域是整个公式 (7) 逻辑操作 and, or, not, (蕴含) (全等) 当谓词应用到的变元是常量或已被束定的变量上时,就叫做句子(sentence)或命题(proposition),谓词变元
3、的个数称作目(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) False Xodd(X) True X(X=2*Y+1odd (X) True XYdivide (X,3,Y
4、,0) False XYdivide (X,3,Y,0) True, 如X =3,Y=1 XYdivide(X,3,Y,0) False, 但很难证明,证明一个全称谓词是比较难的,因为最可靠的证明方法是枚举例证。 于是采取反证的方法,全称量化的谓词取反 量化谓词 取反 Xodd(X) Xnot odd(X) 1 Xodd(X) Xnot odd(X) 2 X(X=2*Y+1odd(X) Xnot(X+2*Y+1odd(X) 3 Xnot(X=2*Y+1)or odd (X) 4 X(X=2*Y+1)and not add(X) 5 XY divide (X,3,Y,0) XY not divi
5、de (X,3,Y,0) 6 XY divide (X,3,Y,0) XY not divide (X,3,Y,0) 7 XY divide (X,3,Y,0) XY not divide (X,3,Y,0) 8,谓词演算的等价变换,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)(P
6、R)化成合取范式 (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), 中间可利用以 这些规则演绎出的定理
7、证明(proof)是个语句序列, 以每个语句得到证明而结束, 即每个句子要么演绎成公理, 要么演绎成前此导出的定理,一个证明若有N个语句(命题)则称N步证明 反驳(refutation)是一个语句的反向证明。 它证明 一个语句是矛盾的, 即不合乎给定的公理 一个语句若能从公理出发推演出来, 则称合法语句, 任何合法语句也叫做定理(theorem) 从某一公理集合导出的所有定理集合称为理论(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),谓词in
9、terval(间隔数)在整数域上有两个子域odd、even都能够满足 间隔数理论不能证明interval(3),也不能证明not interval(3)为真命题这就是Milbert讨论过的可判定(decidability)问题.1936年Church和Turing证实谓词演算可判定性问题是没有解的 一旦我们断言interval(3)或interval(2)是真命题,我们立刻可通过演绎证明按这个理论写出的每一个谓词为真.这就是Godel和Herbrand1930年证实的谓词演算具备的完整性(completeness),证明技术 从谓词演算具有完整性, 理论上可证明按公理集合建立的任何理论。 关键
10、是效率。 如果我们从公理出发做出每一个步骤, 在新的步骤上仍然要查找每一个公理,找出可能的推理。如此下去就形成一个庞大的树行公理集, 每层的结点表示一个公理的语句, 其深度和宽度随问题和最初给出的公理而定, 一层一步骤, N层的树就是N步推理。 对于自动定理证明程序, 只有穷举每条可能的证明步骤才能说它是完全的。 穷举完所有路径马上遇到组合爆炸问题,无论是深度优先还是广度优先,百步演绎可能的路径数都是天文数字。,归结定理证明 J.A.Robinson1965年提出的归结法(resolution) ,是命题演算中对合适公式的一种证明方法。 为了证明合适公式F为真, 归结法证明F恒假来代替F永真。
11、把两子句合一(unification)并消去一对正逆命题,故归结也译作消解。归结证明的过程并称之归结演绎, 其步骤如下:,1把前题中所有命题换成子句形式。 2取结论的反,并转换成子句形式,加入1中的子句集. 3在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句(归结式),再加入到子句集。 4重复3,若归结式为空则表示此次证明的逻辑结论是矛盾,原待证结论若不取反则恒真。命题得证。 否则继续重复3。,例:归结证明 若有前题 待证命题 取反得新子句 p1 QP PU p5 P p2 RQ p6 U p3 SR p4 US 取待证命题的反, 得PU, 它是连接的两个子句P、U,把它们加到前题子
12、句集, 为p5,p6。,归结演绎如下图: QP P p1-p5归结 Q RQ 再与p2归结 SR R 再与p3归结 S US 再与p4归结 U U 再与p6归结 矛盾,由本例可以看出两个问题: 第一,归结法是由合一算法实现的。所谓合一是找出型式匹配的两子句, 将它们合一为归结式, 相当于代数中的化简。 第二,如果得不出矛盾,那么归结法要无休止地做下去,中间归结式出得越多, 匹配查找次数越多, 每一步都做长时间计算, Solution:利用切断(cut)操作, 并利用对子句形式进一步限制的超级归结法(Hyperresolution)。,Horn子句实现超归结 Horn子句是至多只有一个非负谓词符
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 逻辑 程序设计语言
链接地址:https://www.31doc.com/p-3222669.html