（系统分析与集成专业论文）若干逻辑自动推理方法研究.pdf

摘要 自动定理证明( a u t o m a t e dt h e o r e mp r o v i n g ) 或者机器定理证明( m e c h a n i c a l t h e o r e mp r o v i n g ) 是通过计算机实现定理证明二十世纪五十年代以来自动定理证 明一直是计算机科学的热点之一，在数学、硬件测试与验证、软件生成与验证、协 议验证、人工智能方面都得到了成功的应用 部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一 阶逻辑的可满足问题，检查子句集的满足式映射中的阻塞是该方法的关键论文提 出的子句搜索方法在判定子旬集可满足性的同时给出了一个模型从而得到满足式 映射格值逻辑的不完全可比性便于描述人类的思维、判断和决策格值命题逻辑 系统l p ( x ) 于1 9 9 3 年建立，目前对l p ( x ) 系统的自动推理研究主要是归结方法，论 文讨论了它的t a b l e a u 方法常用的逻辑证明方法重点在于判定可满足性而不能给 出符合人们阅读习惯的演绎过程归结方法、语义表方法、相继式方法是定理证明 中的常用方法，但是重点在于判定而不是演绎，论文探讨了相干命题逻辑系统r 的 试探法实现和相干自然推理系统n r 的自然推理法实现，生成了类似于手工证明的 可读证明具体而言论文的工作包括以下几方面： ( 1 ) 提出了子旬搜索方法判定命题子句集的可满足性并给出可满足子句集的一 个模型子句搜索方法通过查找到子句集不可扩展的子句c 来判定的可满足 性结合部分实例化方法将子句搜索方法提升至一阶，分离了谓词公式的结构和变 量，从而提高合一算法的效率并节省了存贮空间用正整数代表原子，负整数代表负 文字，简化了算法实现 ( 2 ) 提出了格值命题逻辑系统l p ( x ) 的t a b l e a u 方法，语义表中的公式都是受限 蕴涵公式通过引入b o u n d s 、b o u n d s ( x ) 和极大相容集证明了其正确性和完备 性对于真值域可直积分解的系统三，p ( x ) ，讨论了其格直积分解证明 ( 3 ) 提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生 了类似于手工证明的演绎序列将公式转化为二叉树的形式存贮于动态数组中减小 了公式冗余，用数组下标代表公式简化了实现 ( 4 ) 提出了应用于自然推理方法的回溯方法先从假设集出发构建证明树，再从 树根节点逐层推导各公式的属性，实现了相干自然推理系统n r 的类似手工证明的 自然推理方法证明 综上所述，论文提出了判定子句集可满足性的子旬搜索方法并将其提升至一 阶，提出了格值命题逻辑系统卯的t a b l e a u 方法，提出了后推试探方法和回溯方 法并实现了相干命题逻辑系统尺的可读证明，在理论和应用方面都有积极意义 关键词：定理证明，自动推理，子句搜索方法，一阶逻辑，格值逻辑，t a b l e a u 方法 试探方法，自然推理方法，可读证明 a b s t r a c t a u t o m a t e dt h e o r e mp r o v i n go rm e c h a n i c a lt h e o r e mp r o v i n gi sc o n c e m e dw i t ht h e b u i l d i n go fc o m p u t i n gs y s t e m st h a ta u t o m a t et h ep r o c e s so fp r o v i n gt h e o r e m s s i n c et h e 19 5 0 sa t ph a sb e e no n eo fa c t i v er e s e a r c ht o p i c so fc o m p u t e rs c i e n c ea n ds u c c e s s f u l l y u s e di nm a t h e m a t i c s ，h a r dt e s ta n dv e r i f i c a t i o n ，s o f t w a r eg e n e r a t i o na n dv e r i f i c a t i o n ，d r o - t o c o lv e r i f i c a t i o n ，a n da r t i f i c i a li n t e l l i g e n c e t h ep a r t i a li n s t a n t i a t i o nm e t h o dr e d u c e ss a t i s f i a b i l i t yp r o b l e m sf o rf i r s t - o r d e rl o g i c t oas e r i e so fg r o u n d - l e v e ls a t i s f i a b i l i t yp r o b l e m s f i n d i n go u tt h eb l o c k a g e so fs a t i s f i e r m a p p i n g sf o rc l a u s es e ti sn e c e s s a r yi nt h i sm e t h o d c l a u s es e a r c h i n gm e t h o dp r o p o s e d b yi i sn o to n l yd e c i d e st h es a t i s f i a b i l i t yo fc l a u s es e tb u ta l s op r e s e n t sam o d e lt h e no b - r a i n sas a t i s f i e rm a p p i n g l a t t i c e v a l u e dl o g i ci sn o tc o m p l e t e l yc o m p a r a b l ea n dp r o p e r t od e s c r i b i n gt h i n k i n g ，j u d g i n ga n dd e c i s i o n m a k i n g l a t t i c e - v a l u e dp r o p o s i t i o n a ll o g i c s y s t e ml p ( x ) i sp r o p o s e di n1 9 9 3 a tp r e s e n ta u t o m a t e dr e a s o n i n gr e s e a r c ha b o u tl p ( x ) f o c u s e so nr e s o l u t i o nm e t h o d ，t h i st h e s i sd i s c u s s e st a b l e a um e t h o df o rl 尸) t h eu s u a l d e d u c t i o nm e t h o d ss u c ha sr e s o l u t i o nm e t h o d ，t a b l e a um e t h o d ，s e q u e n tc a l c u l u se t ce m p h a s i so nd e c i d a b i l i t yi n s t e a do fd e d u c t i o n t h i st h e s i sd i s c u s s e si m p l e m e n t i n gp r o b i n g m e t h o da n dn a t u r a ld e d u c t i o nm e t h o df o rr e l e v a n tp r o p o s i t i o n a lr ，a n dg e n e r a t e sr e a d a b l e d e d u c t i o ns e q u e n c e ss i m i l a rt oh u m a n s n em a i nc o n t e n ti sa sf o l l o w s ： ( 1 ) p r o p o s i n gc l a u s es e a r c h i n gm e t h o dw h i c hd e c i d e ss a t i s f i a b i l i t yo fc l a u s es e t a n dp r e s e n t sam o d e lf o rs a t i s f i e ds e t n i sm e t h o dd e c i d e ss a t i s f i a b i l i 哆b ys e a r c h i n go n e c l a u s ew h i c hc a nn o te x t e n d e df r o m 西u p d a t i n gc l a u s es e a r c h i n gm e t h o dt of i r s t - o r d e r b yu s eo fp a r t i a li n s t a n t i a t i o nm e t h o d s t h i st h e s i ss e p a r a t e sp r e d i c a t ef o r m u l a ei n t ot w o p a r t s ：s t r u c t u r e sa n dv a r i a b l e sh e n c ei m p r o v e su n i f i c a t i o na l g o r i t h me f f i c i e n c ya n ds a v e s s t o r a g es p a c e w ee s t a b l i s ham a p p i n go fo n ea t o mo n t oo n ep o s i t i v ei n t e g e ra n do n e n e g a t i v ew o r do n t oo n en e g a t i v ei n t e g e r ( 2 ) p r o p o s i n gt a b l e a um e t h o df o rl a t t i c e - v a l u e dp r o p o s i t i o n a ls y s t e mz 尸( 抑，a n d a l lf o r m u l a ei sb o u n d i n gi m p l i c a t i o n s b yi n t r o d u c i n gc o n c e p t ss u c ha sb o u n d s ( x ) ， b o u n d s a n dm a x i m a l l yc o n s i s t e n ts e t , w ep r o v et h i sm e t h o d sc o r r e c t n e s sa n dc o m - p l e t e n e s s i ft r u t hv a l u es p a c elo fs y s t e ml p ( x ) i st h ed i r e c tp r o d u c to fl i ，t h e nw ec a n p r o v et h e o r e m si nl p ( x ) b ym e a n so fd i r e c td e c o m p o s i t i o n ( 3 ) p r o p o s i n gb a c k w a r dp r o b i n gm e t h o d ，o b t a i n i n gap r o o ft r e ec o n s i s t i n go ff o r - m u l a ei nd e d u c t i o ns e q u e n c e s ，a n dg e n e r a t i n gr e a d a b l ed e d u c t i o ns e q u e n c e ss i m i l a rt o h u m a n s w er e d u c ef o r m u l a er e d u n d a n c yb yt r a n s f o r m i n gf o r m u l a ei n t ob i n a r yt r e e f o r m sa n ds t o r i n gt h e mi nad y n a m i ca r r a y , t h e na r r a ys u b s c r i p t ss t a n df o rf o r m u l a e 1 1 1 ( 4 ) p r o p o s i n gb a c k t r a c em e t h o da p p l i e dt on a t u r a ld e d u c t i o nm e t h o d f i r s t l yc o n 。 s t r u c t i n gap r o o f t r e ef r o mh y p o t h e s i ss e t ，t h e ns t a r t i n gf r o mt r e er o o tw eo b t a i nf o r m u l a e a t t r i b u t e sl a y e rb yl a y e r t h et h e s i si m p l e m e n t sn a t u r a ld e d u c t i o nm e t h o df o rr e l e v a n t n a t u r a ld e d u c t i o ns y s t e mn ra n dg e n e r a t e sr e a d a b l ed e d u c t i o ns e q u e n c e ss i m i l a rt oh u 。 m a n s i nc o n c l u s i o n ，t h i st h e s i sp r o p o s e sc l a u s es e a r c h i n gm e t h o dt oc h e c ks a t i s f i a b i l i t yo f c l a u s es e t ，l i f t st h en e wm e t h o dt of i r s t - o r d e r , p r o p o s e st a b l e a um e t h o d f o rl a t t i c e d v a l u e d l o g i cs y s t e ml p ( x ) ，p r o p o s e sb a c k w a r dp r o b i n gm e t h o d a n db a c k t r a c em e t h o d ，g e n e r a t e s r e a d a b l ep r o o ff o rr e l e v a n tp r o p o s i t i o n a ll o g i ca n dh a sap o s i t i v em e a n i n gi nt h et h e o r y a n da p p l i c a t i o n k e yw o r d s ：t h e o r e mp r o v i n g ；a u t o m a t e dr e a s o n i n g ；c l a u s es e a r c h i n gm e t h o d ； f i r s t - o r d e rl o g i c ；l a t t i c e d ，v a l u e dl o g i c ；t a b l e a um e t h o d ；p r o b em e t h o d ；n a t u r a ld e d u c t i o nm e t h o d ；r e a d a b l ep r o o f 学位论文独创性声明 本人所呈交的学位论文是在我导师的指导下进行的研究工作及取得的研究成 果据我所知。除文中已经引用的内容外，本论文不包含其他个人已经发表或撰写的 研究成果对本文的研究做出重要贡献的个人和集体，均已在本文中作了明确的说 明并表示谢意 作者签名辎日期：芈 学位论文使用授权声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学校有权保留学 位论文并向国家主管部门或指定机构送交论文的电子版和纸质版有权将学位论文 用于非赢利目的的少量复制并允许论文进入学校图书馆被查阅有权将学位论文的 内容编入有关数据库进行检索有权将学位论文的标题和摘要出版保密的学位论 文在解密后适用本规定 学位论文作者签名 日期 导师签名： 第一章绪论弟一早珀了匕 人工智能是二十一世纪三大尖端技术之一，目前已经深入到人们生活的各个 领域并不断地发展它大大提高了社会生产力，使人们生活发生了翻天覆地的变化 i n t e m e t 的高速发展给人工智能提供了前所未有的发展机遇，同时也提出了新的挑 战。人类对知识的获取、表示和利用提出了越来越高的要求自动推理是人工智能 研究的核心内容，其理论和技术是演绎数据库、硬件验证、软件规约与验证、程序 综合、专家系统、智能主体、智能机器人等研究领域的重要基础 1 1自动推理的发展简史 什么是自动推理呢? 按照首届h e r b r a n d 奖获得者l w o s 的说法：自动推理 就是研究用计算机帮助人们进行推理，而这些推理是问题求解时所需要的那些 推理机器定理证明( m e c h a n i c a lt h e o r e mp r o v i n g ，简称m t p ) 1 或自动定理证明 ( a u t o m a t e dt h e o r e mp r o v i n g ，简称a t p ) 2 ，3 ，5 】是自动推理研究中一个重要研究方 向，目的是实现定理证明的机械化 逻辑是关于推理的科学，其历史可以追溯到古希腊机器自动推理的梦想起源 于g w l e i b n i z ，他崇尚严密、精确的数学方法，试图用数学的方法来构建逻辑，为 此他提出了“普遍的符号语言”和“思维的演算”的构想“普遍的符号语言”是一 种表意的通用符号语言，每一个符号明确表达一个概念，在此语言基础上在建立一 种“思维的演算”能够进行逻辑推理的演算g w l e i b n i z 本人没有实践这一宏伟构 想，但是他的创造性思想为现代逻辑的发展指明了方向 现代逻辑的实际创建者是德国学者g f r e g e 1 8 7 9 年他在概念文字，一种按算 术语言构成的纯思维的符号语言一书中，建构了第一个公理化的逻辑演算体系， 被称之为经典逻辑或数理逻辑，内容包括经典命题演算和经典谓词演算g f r e g e 不 仅是数理逻辑的直接先驱，而且是形式化语言包括计算机程序设计语言的先驱 1 9 0 0 年d h i l b e r t 在巴黎国际数学家大会上做了题为“数学问题 的著名演讲 他提出的2 3 个数学难题之一是判定问题( d e c i s i o np r o b l e m ) ，所谓判定问题，用逻辑 学的术语加以陈述是：给定一个任意的谓词逻辑公式的集合a 及任意一个谓词公 1 1 f 朗臻冽 内发瞧简r 史 镣章臻论 式8 ，是否存在一个算法，能对命题“b 是a 的逻辑结论”给卅“是”或“否”的回答 d h i l b e r t 提出的判定问题是诱人的：如果存在一个通用的判定算法，那么就再也不 存在悬而未决的问题了，因为所有的命题都将会被证实或推翻；不再需要天才了，因 为任何个判定问题都将由这个“万能推理机”机械地给出证明过程随后人们朝 这个方向进行不懈地努力 1 9 1 5 年l l o w e n h e i m 与t s k o l e m 同时首次研究了逻辑公式的满足性问题 ( s a t i s f i a b i l i t yp r o b l e m ) ，他们的研究工作表明，给定一组逻辑公式，在从这组公 式构造出的特定解释下，可以证明这组逻辑公式的协调性问题( c o n s i s t e n t ) l l o w e n h e i m 与t s k o ! e m 的研究工作也为后来的k g 6 d e l 及h h e r b r a n d 的研究 指明了方向在1 9 3 0 年k g 6 d e l 和h h e r b r a n d 的博士论文中，他们首次提出了 谓词演算的一个极为重要的概念，即“完备性”概念( c o m p l e t e n e s s ) k g 6 d e l 和 h h e r b r a n d 的研究同时表明了谓词演算的证明机构可以形式化地给出任意一个逻 辑真的命题的证明过程，并都给出了一个发现证明的构造性方法谓词演算的完备 性概念沟通了逻辑真的形式化可证的语法属性与语义属性的联系对于一个逻辑公 式，精确的形式化语法与形式化语义对逻辑真的形式可证性的研究是同等重要的 然而在1 9 3 4 年以前，这方面的工作主要集中在形式化语法方面，而没有涉及到形式 化语义方面直到a t a r s k i 在1 9 3 4 年介绍了谓词演算的严格的形式化语义理论一 包括可满足性、真值、逻辑结论及其它有关概念的精确定义一以后，谓词演算理论 才得以完善 1 9 3 1 年数理逻辑学家k g 6 d e l 提出了著名的不完备性定理【6 】( i n c o m p l e t e n e s s t h e o r e m ) ，该定理断言：即使在初等数论的范围内，对所有命题进行判定的算法也 是不存在的a c h u r c h 与a m t u r i n g 的工作【7 ，8 】的工作表明，对于b 确实是a 的 逻辑结论的情形，存在证明过程给出“是”的结论；但如果b 不是a 的逻辑结论则 不存在也不可能存在证明过程给出“否”的结论也就是说谓词逻辑是不可判定的 ( u n d c c i d a b l c ) g 6 d e l 不完备性定理以及a c h u r c h 与a m t u r i n g 的工作宣告了“万能推理机” 幻想的破灭尽管谓词逻是不可判定的，幸好它还是半可判定的，即对于b 确实是a 的逻辑结论的情形，存在证明过程给出“是”的结论并且，尽管谓词逻辑是不可判 定的，但毕竟还存在着许多可判定的子类【9 】- 【1 1 】因此，人们关于机器证明与自动 推理的努力仍在继续 随着计算机在1 9 4 6 年的问世，定理自动证明的工作主要集中在寻求计算机 可在有限时间内实现的判定算法的计算机实现1 9 5 6 年a n e w e l l ，j c s h a w 和 h a s i m o n 发表了著名论文逻辑理论机【1 2 ，这篇论文促使了1 9 6 5 年d r a t m o u t h 人工智能讨论会的召开这次会议标志着人工智能的诞生逻辑理论机成功地证明 了数学原理中的3 8 个定理这项研究工作提出了表处理这个人工智能的概念， 2 第。章绪论 1 1 自动推理的发疑钧也 开创了a t p 研究领域 1 9 5 9 年h g e l e r n t e r 等人做了几何定理机器证明机( g e o m e 竹t h e o r e mp r o v i n g m a c h i n e ，简称g t m ) 4 i g t m 能够证明直线图形中的大部分高中考试问题 在g t m 产生的同时，出现了在逻辑上建立定理证明机器的第一次努力，即 p c g i l m o r e 和王浩的研究工作他们的工作从经典逻辑的证明过程中总结出推导 推着，机械地去证明谓词演算中的定理1 9 5 9 年p c g i l m o r e 1 3 ，1 4 】发表的证明程 序，是对谓词演算的第一个可用的机械证明程序王浩 1 5 】于1 9 5 8 年在i b m 开 始，并于1 9 5 9 1 9 6 0 年在b e l l 实验室继续关于a t p 的研究工作他研制出三个程 序：第一个程序是关于命题演算的；第二个程序是关于谓词演算中的可判定部分； 1 9 5 9 1 9 6 0 年研制出的第三个程序是对整个谓词演算的g i l m o r e 方法的理论基础 是h e r b r a n d 定理，即为了证明谓词演算中的某一公式的恒假性，转化为证明一个 命题公式的恒假性而证明一个命题公式的恒假性时，p c g i l m o r e 采用了最原始 的“乘法方法” 1 9 6 0 年m d a v i s 和h p u t n a m 对p c g i l m o r e 方法做了改进，提出d p 过程【1 6 d p 过程仍以h e r b r a n d 定理为基础，只是在证明一个命题公式的恒真性时，采用了 一些技巧如：t a u t o l o g y 规则，单文字规则，纯文字规则，分裂规则等但是，d p 过程 对g i l m o r e 方法的这种改进不是本质的，因为这两种方法都需要枚举基替换去产生 恒假的命题公式 1 9 6 0 年d p r a w i t z 1 7 1 发表论文指出了d p 过程的这个致命弱点并给出了改进 d p r a w i t z 方法不再是枚举替换去产生恒假的命题公式，而是主动去寻找产生这个 恒假命题公式的那个替换d p r a w i t z 的“直接寻找替换，从而避免产生公式的组合 爆炸”这个思想是深刻的，这里使用了人工智能中的匹配技术但是d p r a w i t z 在实 现这种想法时，却很不理想 1 9 6 0 年前后的三年时间是a t p 领域中逻辑方法的一段重要时间基于 h e r b r a n d 定理的g i l m o r e 方法，d p 过程中的单文字规则和d p r a w i t z 的匹配思想。 最终导致了归结原理( r e s o l u t i o np r i n c i p l e ) 的产生1 9 6 4 年j a r o b i n s o n 给出了简 洁的归结原理【1 8 】被j a r o b i n s o n 用归结原理所形式化的逻辑里，没有公理，只有 一条使用合一( u n i f i c a t i o n ) 替换的推导规则如此简洁的逻辑系统，却是谓词演算中 的一个完备系统，即任意一个恒真的一阶公式，在j a r o b i n s o n 的逻辑系统中都是 可证的归结原理的重要改进工作有如下一些： 1 9 6 4 年l w o s ，d c a r s o n 和g r o b i n s o n 提出了单文字子句优先策略和支撑集 策略【1 9 】 1 9 6 5 年j a r o b i n s o n 提出了超归结方法【2 7 】 1 9 6 7 年j r s l a g l e 提出了语义归结【2 1 1 9 6 8 年d w l o v e l a n d 和d l u c k h a m 提出了线性归结【2 0 ，2 3 】 3 1 1 f t j j j 推理的锭蜓简殳第。章绪论 1 9 7 0 年r b o y e r 提出锁归结【3 0 1 1 9 7 0 年r a k o w a l s k i 和d k u e h n e r 提出了s l 归结【2 2 1 1 9 7 0 年c l c h a n g 提出输入归结【2 4 1 ，并且证明了它和单元归结【2 5 】是等价 的 1 9 8 2 年n v m u r r a y 提出了n c 归结【2 6 1 1 9 6 8 年l w o s 和g r o b i n s o n 提出了一种和归结方法相容的处理等式的方法 即调解方法【4 7 1 9 7 8 年至1 9 9 2 ，吉林大学以王湘浩和刘叙华为代表的研究者提出了一些改进 【3 2 1 一 4 0 1 ，如锁语义归结，线性半锁归结，输入锁归结，单元锁归结，输入对称调解， 输入有向调解，广义归结，广义调解和广义h o r n 集上的归结，以及算子模糊逻辑中 的九归结，九调解，广义九归结和广义九调解等陆汝钦等人提出了正单项有序归结 和有序输入归结【2 8 ，2 9 王元元在广义替换归结【4 l 】陆汝占提出了着色归结【4 3 归结方法对一个包括一系列集合的交的简单问题的证明非常笨拙，w w b l e d s o e 对归结方法的能力产生了怀疑于是以w w b l e d s o e 为首的集体开始了关于类人 方法的a t p 的最有成就、最持久的努力1 9 7 7 年w w b l e d s o e 发表了重要论 文( n o n - r e s o l u t i o nt h e o r e mp r o v i n g ) ) 【48 】 1 9 7 0 年d e k n u t h 和p b b e n d i x 提出了重写规则【4 9 所谓重写规则就是代换 规则，亦即将一个等式右侧出现的规则去代替左端出现的规则，重写规则法处理等 式中的推理问题特别有效d e k n u t h 和p b b e n d i x 使用重写规则法，解决了群论中 的一些不等式证明问题7 0 年代末，d s l a n k f o r d 等人建立布尔代数的标准重写系 统，解决了重写规则法在命题逻辑中的应用8 0 年代初，j h s i a n g 等人建立对一阶逻 辑的使用重写规则法的定理证明系统l w o s 的等式调解法，实际上也是一种重写 规则 a c h u r c h 与a m t u r i n g 的工作表明谓词逻辑是不可判定的因而。人们退而求 其次。寻找表达力较弱但是可判定的谓词逻辑的子集，以及进一步在可判定子集中 寻找存在有效算法的( 计算复杂度低) 的子集近年来，人们定义了或识别了各种新 的可计算逻辑f 5 0 1 一【5 7 】，提出了新的知识表示模型与推理方法，如基于模型的表示 与推理方法【5 8 【6 3 】，基于学习的模型表示与推理方法【6 4 6 8 】等其中基于模型 的表示与推理方法与常用的c n f ( c o n j u n c t i v en o r m a lf o r m ) 表示方法相比，在外展 推理( a b d u c t i o nr e a s o n i n g ) 方面取得了一些令人欣喜的成果 我国学者在几何代数自动证明方面取得了令人瞩目的成就吴文俊【6 9 ，7 0 】提 出了几何定理机器证明的“吴方法 7 0 年代，吴文俊由中国传统数学中的机械化 思想出发，从几何定理证明入手开始数学机械化研究，所建立的数学机械化方法，为 国际自动推理的研究开辟了新的前景经过近2 0 年的努力。几何定理自动证明的吴 方法及在其影响下产生的一系列重要的新方法，已经发展成具有我国特色且在国际 4 笫一学绪沦 1 2 啦经舆逻辑研究溉况 上领先的数学机械化理论，形成了自动推理与方程求解的中国学派数学机械化理 论以代数与微分方程求解的吴一r i t t 零点分解定理【7 0 】为核心高小山【7 l 】 7 3 】则 在8 0 年代把他的理论在计算机上用几秒钟的时间变成了现实，拉近了数学机械化 理论与人类工作和生活的距离在此基础上，高小山又发明了一种称之为“结构性 数据库”的推理方法，解决机器证明时的几何对称性问题，用以提高机器证明的质 量不久，他的这一方法再次被普遍应用于物理、机器人和教学中张景中【7 4 7 6 】 提出了面积解题方法，创立计算机生成几何定理可读证明的原理和算法，创立定理 机器证明的数值并行方法的原理和算法等杨路【7 7 8 0 】在不等式自动发现与机 器证明方面作出卓越的工作曾振柄、符红光、冯勇【8 1 一 8 6 】等在以符号和数值计 算为基础解决自动推理和定理机器证明难题方面取得了一系列成果 定理自动证明的另一个重要方面是定理自动证明器的建造和应用【1 5 6 目前， 已经设计出许多基于不同方法的定理证明器【4 4 ，4 5 ，4 6 ，8 7 ，8 8 ，8 9 定理自动证明 技术已成功应用的领域有逻辑学、数学、计算机科学、工程技术、社会科学；潜在 的应用领域还有生物科学、医学、商业这些应用系统使用的语言是经典一阶逻辑， 或非经典逻辑，甚至高阶逻辑如使用一阶语言的系统有o t t e r , s e t h e o ，s p a s s ；。 s p t h e o ，w a l d m e r s t e r ；使用高阶语言的系统有c o q ，h o l ，n q t h m 虽然a t p 的应用 还处于初期，但是应用前景十分广阔 1 2 非经典逻辑研究概况 专家系统和知识工程的出现使人们认识到仅仅研究那些从真前提得出真结果 的那种古典逻辑推理方法是不够的因为人类生活在一个充满不确定信息的环境里 进行着有效的推理因此，为了建立真正的智能系统，研究那些更接近人类思维方式 的非单调推理、模糊推理等，就变得越来越必要了，非经典逻辑逻辑应运而生“非 经典逻辑”泛指不同于经典命题演算和经典谓词演算的逻辑系统非经典逻辑总体 上可以划分为两大类：一类是与经典逻辑平行的逻辑系统，如直觉逻辑、多值逻辑 和模糊逻辑：一类是对经典逻辑做了扩充的逻辑系统，如模态逻辑和时态逻辑 与经典逻辑平行的非经典逻辑系统使用的语言与经典逻辑的语言基本相同区 别在于经典逻辑中的一些定理在这类非经典逻辑中不再成立，直觉主义逻辑和标准 三值逻辑系统中“排中律不再成立对经典逻辑进行扩充的非经典逻辑系统一般 都承认所有经典逻辑中存在的定理的基础上，在两个方面对经典逻辑扩充：一是扩 充了经典逻辑的语言：二是扩充了经典逻辑的定理例如，模态逻辑增加了两个逻辑 算子l ( 必然) 和m ( 可能) ，从而扩大了经典逻辑的词汇表 1 9 2 0 年j l u k a s e i w i c z 9 0 】提出了三值逻辑系统，这是多值逻辑的第一个形式 5 1 3 论文的逸退和1 t 耍- e f t 箱。蘩绪论 系统，第三个值解释为“可能的”或“未确定的”，表示未来可能发生的状态随后， j l u k a s e i w i c z 又将他的三值逻辑系统推广到了n 值及无穷值 1 9 2 1 年e p o s t 9 1 】独立地发展了他提出的有穷多值逻辑系统，它是以二值逻辑 作为特例的纯形式的逻辑系统 d a b o c h v e r 9 2 】在1 9 3 9 年提出了他的三值逻辑系统，该系统有命题和句子之 分，可以为真，为假，也可以无意义 1 9 5 2 年s c k l e e n e 9 3 】给出了强三值逻辑系统和弱三值逻辑系统 1 9 6 5 年，l a z a d e h 【9 4 】提出模糊集合论以后，人们逐渐认识到它对非经典逻 辑的研究具有重要意义，模糊逻辑与模糊推理的研究随之得到了迅速发展模糊逻 辑的真值域取在一个普通的偏序集合或全序集合上，用以描述模糊概念 1 9 6 9 年，j a g o g u e n 9 5 】在完备的格序半群上提出了第一个格值逻辑的形式系 统，其真值域l 为一个完备的格序半群 1 9 7 9 年，j p a v a l k a 9 6 一 9 8 】将真值加入语言中，以丰富剩余格l 为真值域，建立 了一个模糊逻辑系统 1 9 8 5 年，朱梧桢，肖奚安【1 0 0 ，1 0 1 】基于中介原则提出了命题逻辑m p 及其扩 展系统m p 木 1 9 8 5 年，刘叙华提出了取真值为语言真值格的格值逻辑系统并讨论了其上的 归结原理【9 9 ，该格值逻辑系统中的蕴涵是k l e e n e 蕴涵，且其中的格要求有分解元 此外，王国俊对模糊逻辑和格值逻辑系统作了一系列重要的研究工作【1 0 2 - 【1 0 4 】 1 9 9 3 徐扬提出格蕴涵代数【1 2 4 】并以此为基础建立了若干逻辑系统1 9 9 3 年 至1 9 9 4 年建立格值命题逻辑系统l p ( x ) 1 3 7 ，1 3 8 ，证明了演绎定理、可靠性定 理、弱完备性定理和协调性定理1 9 9 6 年至1 9 9 7 年，建立并格值一阶逻辑系统 l f ( x ) 1 3 9 ，1 4 0 ，1 9 9 7 年至2 0 0 1 年提出了分层的格值命题逻辑系统厶p l 1 4 1 】和 l ，t 1 4 2 ，1 4 3 ，证明了相应的( 口，p ，y ) 一演绎定理、口一可靠性定理、( 口，励一完备性定 理和( 口，所一协调性定理 冯棉【1 0 5 】讨论了道义逻辑、模态逻辑、和时态逻辑，周昌乐【1 0 9 】对模态命题 逻辑、命题时态逻辑、模态谓词逻辑做了详细的阐述 1 3 论文的选题和主要工作 r j e r o s l o w 和j n h o o k e r 提出的部分实例化方法把一阶问题化为一系列命题 逻辑中的可满足性问题来解决一阶逻辑的可满足问题部分实例化方法需要检查阻 塞或潜在阻塞，其中检查阻塞要求子旬集可满足性判定算法能给出一个满足式映 射，论文提出的子句搜索方法在判定子旬集可满足性的同时给出了一个模型从而得 6 第一章绪论 1 3 论文的选题和。要1 ：作 到一个满足式映射，不需要检查潜在阻塞因而简化了实现部分实例方法的实现在 多值逻辑中，对格值逻辑的研究具有特殊的意义，主要表现在：其一，它将链型真值 域推广到更一般的格；其二，格中的不完全可比性便于描述人类的思维、判断和决 策徐扬等于1 9 9 3 年提出了格蕴涵代数，建立了格值命题逻辑系统l p ( x ) ，深入研 究了l p ( x ) 的性质，取得了丰硕的研究成果目前对l p ( x ) 系统的自动推理研究主 要是归结方法，论文讨论了它的t a b l e a u 方法常用的逻辑证明方法重点在于判定可 满足性而不能给出符合人们阅读习惯的演绎过程而演绎过程至关重要，是研究逻 辑学的初衷a g h a m i l t o n 指出【1 5 8 ：“研究逻辑学的目的在于一至少部分在于 一分析演绎过程”论文探讨了相干命题逻辑系统尺的试探法实现和相干自然推 理系统n r 的自然推理法实现，生成了类似于手工证明的可读证明 论文分为五章，内容如下： 第一章绪论，简介了自动推理的历史和非经典逻辑的研究概况 第二章一阶子句搜索方法及其实现提出了子旬搜索方法，该方法查找一个子 句集不可扩展的子句c ，若c 存在，子句集可满足，否则不可满足与归结法不 同的是，该方法在判定可满足性的同时还给出了一个模型子旬搜索方法结合部分 实例化方法实现了一阶可满足性的判定精心设计了数据结构：建立文字与整数的 映射表，互补对对应的2 整数之和为0 ；分离谓词公式的结构与变量，降低算法的时 间和空间复杂度 第三章格值命题逻辑系统l p ( x ) 的t a b l e a u 方法和直积分解证明目前针对 l p ( 柳系统的自动推理研究主要是归结方法，论文提出了它的t a b l e a u 方法，通过引 入受限蕴含公式和极大相容集等概念给出了其正确性和完备性证明对于真值域可 直积分解的系统l p ( x ) ，应用格直积分解的方法将其中的定理证明转化为多个小规 模系统厶p ( 抑中的证明 第四章相干命题逻辑系统r 的后推试探方法证明、相干自然推理系统n r 的 自然推理法证明和两种推理方法的混合证明，产生了类似于手工证明的可读演绎序 列论文提出的后推试探法将命题的求证分解为一或二个命题的求证，这个过程是 递归的，命题之间在逻辑上构成一棵证明树，当树的叶子节点为公理、定理或前提 时，原命题得证提出了针对自然推理方法的回溯方法，当待证公式a 得证后，从其 证明树根节点出发反向确定证明序列中各公式的属性，包括：确定各公式的秩、调 整同一假设嵌套、标识重述规则、删除重复公式、调整相干标记求证过程会产生 大量的中间公式且相当部分的公式会重复出现，为了简化实现和避免冗余，将公式 映射成数字串并转化成二叉树的形式，二叉树各节点存贮在一维数组c o m m o n l i s t 中并保持唯一 第五章总结与展望，回顾了论文的工作，对后续的完善工作进行了展望 7 第二章一阶子句搜索方法 可满足性问题是当代理论计算机科学中的重要问题，是著名的n p 完全问题 目前的主要的判定方法有归结方法、d p 方法等本章提出了子句搜索方法，通过查 找找到子句集西不可扩展的子句判定的可满足性，在可满足的情况下，给出了垂 的一个模型部分实例化方法把一阶问题转化为一系列命题逻辑中的可满足问题来 解决一阶逻辑的可满足性问题结合部分实例化方法，将子句搜索方法提升至一阶 2 1 1 关于子句集 2 1 子句搜索方法 可满足问题( 简称s a t ) 是：对于一个命题逻辑公式，是否存在对其变元的一个 赋值使之成立? 这个问题在许多领域都有重要的意义在知识库维护中，当知识以 逻辑公式的形式表达时，知识库的一致检查可以归结为命题逻辑公式的可满足性 在开放逻辑中，新事实是否与已有