（计算机软件与理论专业论文）基于逻辑的自动推理研究.pdf

摘要 自动推理是一门在给定知识及有关推理策略的前提下，研究用计算机帮助人们进 行推理的学科。自动推理的理论和技术是演绎数据库、软件规约与验证、专家系统、 智能主体、智能机器人等研究领域的重要基础。进入二十世纪九十年代以来，特别是 w e b 时代的到来，自动推理又面临着新的使命与挑战。在前人工作的基础上，对自动 推理领域的如下问题进行了研究与探索：基于归结原理的多种类谓词演算、模糊逻辑 与近似推理、w e b 环境下的知识表示与自动推理等。 多种类逻辑及多种类谓词演算是经典一阶逻辑及其演算的重要拓展，并已经在计 算机科学的诸多领域得到了广泛运用，如知识表示、程序设计语言、软件规约与验证 等。与基于归结原理的经典谓词演算相比，多种类谓词演算具有更高的演绎效率。为 进一步提高演绎效率与简化计算机程序设计结构，提出了一种基于归结原理的多种类 谓词演算的演绎策略，即r l d ( r i 【g h t m o s tl i n e a rd e d u c t i o n ) 演绎，并证明了它的完 备性。实现了基于r l d 演绎的多种类谓词演算的一个原型系统并成功求解了著名的人 工智能问题，即s t e a m r o l l e r 问题。 包含性概念及包含性测试算法不仅在提高演绎效率方面具有重要的作用，而且在 软件工程形式化方法方面也具有重要的意义。文中指出了子句包含关系与蕴涵关系的 非等价性，给出并证明了命题“若c 蕴涵d 成立，则c 包含d ”成立的一个充分条件。 初步探讨了多种类谓词演算及r l d 演绎在软件构件表示与检索方面的应用前景。 模糊集与模糊逻辑已成为处理现实生活中大量存在的不确定性及模糊性信息的重 要数学工具。针对所讨论问题的具体领域，利用问题域中元素的各种特殊关系来提高 推理效率，历来是自动推理领域研究的重要方向之一。相似性关系是模糊集理论中的 基本概念，也是应用最为广泛的基本关系之一。当相等约束不能满足从而需要进行适 当放松时，相似性关系是合适的候选者。相似性关系在需要将相等约束放松的研究领 域中得到了广泛的应用，如近似推理。为了在模糊逻辑中集成相似性关系并考虑其近 似推理，把相似性关系看成是一种模糊相等关系，提出了一种带有相似性关系的模糊 逻辑，给出了带有相似性关系的模糊逻辑的语法及语义结构。 调解规则是在带有相等关系的经典谓词演算中提出的推理规则，它能够进行高效 的等值推理。将调解规则拓展到了带有相似性关系的模糊逻辑谓词演算，讨论了基于 归结与调解规则的近似推理。给出并证明了基于归结与调解方法的近似推理的有关属 性，证明了如果子旬集s 中的每个子句蛉真德都大于0 5 ，那么从s 中使用归结与 ( 或) 调躲砉萋爨揍密戆任意一个逻辑结莱臻楚套效愆。考虑虱诲多舞动整理帮逮题餐 决系统均是基于否证法，证髑了基于归结与调解娩刚对模糊谓词演算的完备性定理。 自动推理系统的性能测试与评价是自动推理领域备受关注的问鼷。为进行公正的 系统评价，需要一系列的评价标准以便测试者做出合理、准确、公正的评价结论。其 中，闷题的表示是其中主要原则之一。为了给爨动推理领域提供个统一的问题表示 鼹式，爨凌了一个基于多耱裳逻辑夔知谖嚣遗落蠹m s k m l ( m a n y - s o r t e dk n o w l e d g e m a r k u pl a n g u a g e ) 。与璃有的舰掰标记语言鞫魄，m s k m l 具有如下特点：一方面， m s k m l 的元素名直接对成于多种类逻辑与归结原理的有关术语，这梯自动推理界可 以很快熟懑m s k m l ，也可以设计一个程序自动蚍将问题的子句集与反驳过程转换成 与其对威的m s k m l 文档；另一方面，m s k m l 不仅能够表示基于经热一阶逻辑的知 谚 ，毽麓袭示基予多糖类递辍的鳃圣哭。 对许多霜户瑟言，或砻不是备开发鑫动推邂系统的有关知识，躐蠢不具备系统资 源，但怒又需要自动推理系统来完成他( 她) 的有关需求。在这种情彤下，分布在i n t e m e t 上的自动摊理系统无疑是丰富的可用资源，他( 她) 可以用这些系统提供的自动推理 w e b 服务来完成自己的任务。使自动推理成为种w e b 服务，既可以为w e b 用户提 供自动撼理服务，也可以便w e b 爝户参与自动攥疆系统的溅试工l 乍，觚覆获褥更丰富 戆实验数爨以便骰塞更为公蒸合理静系统评徐。斑了绘w e b 援户撬谈囊葫摇瑾w e b 服务，构造了个自动推理系统p r o v e r ，p r o v e r 实现了基于r l d 演绎的多种类谓词演 算，采用简单对象访问协议s o a p ( s i m p l eo b j e c t a c c e s sp r o t o c 0 1 ) 作为服务器与w e b 用户问的网络通信协议，并用w 如服务描述谮畜w s d l ( w e bs e r v i c ed e s c r i l ：i t i o n l a n g u a g e ) 对系统提供的w e b 服务加以描述。 关键词：人工智能自动推理谓词演算模糊逻辑归结原理 知识标记万维网服务 a b s t r a c t a u t o m a t e dr e a s o n i n gi sc o n c e r n e dw i t l lt h ed e v e l o p m e n ta n du s eo fs y s t e m st h a t a u t o m a t es o u n dr e a s o n i n g ：t h ed e r i v a t i o no fc o n c l u s i o n st h a tf o l l o wi n e v i t a b l yf r o mf a c t s a u t o m a t e dr e a s o n i n gi sa l li m p o r t a n tt h e o r e t i c a lf u n d a m e n tf o rm a n ys u b f i e l d so f c o m p u t e r s c i e n c e ，s u c ha sd e d u c t i v ed a t a b a s e ，s o t t w a r es p e c i f i c a t i o na n dv a l i d a t i o n ，e x p e r ts y s t e m ， a g e n t ，i n t e l l i g e n tr o b o t i c s ，e t c i nt h i st h e s i s ，t h ef o l l o w i n ga u t o m a t e dr e a s o n i n gi s s u e sa r e r e s e a r c h e d ：m a n y - s o r t e dp r e d i c a t ec a l c u l u s ，f u z z yl o g i ca n da p p r o x i m a t er e a s o n i n g ，a n d k n o w l e d g er e p r e s e n t a t i o na n da u t o m a t e dr e a s o n i n g o nt h ew e b r e s o l u t i o n b a s e dm a n y - s o r t e dp r e d i c a t ec a l c u l u sh a sb e e na p p l i e dt om a n yf i e l d so f c o m p u t e rs c i e n c e ，s u c ha sk n o w l e d g er e p r e s e n t a t i o n ，a r t i f i c i a li n t e l l i g e n c ea n da u t o m a t i c t h e o r e mp r o v i n g ，s o f t w a r es p e c i f i c a t i o na n dv e r i f i c a t i o n ，e t c c o m p a r e dw i t ht h ec l a s s i c a l r e s o l u t i o n b a s e dp r e d i c a t ec a l c u l u s ，t h em a n y - s o r t e do n eh a sam o r ee f f i c i e n td e d u c t i o n s y s t e m i nt h i st h e s i s ，i no r d e rt of u r t h e ri n c r e a s et h ed e d u c t i o ne f f i c i e n c ya n ds i m p l i f yt h e p r o g r a n l i m i n gs t r u c t u r e ，al i n e a rd e d u c t i o n ，i e ，r l d ( a b b r r i g h t m o s tl i n e a rd e d u c t i o n ) ，i s p r o p o s e da n di t sc o m p l e t e n e s si sp r o v e d ap r o t o t y p es y s t e mo fm a n y s o r t e dl o g i cw i t h r l di si m p l e m e n t e da n daw e l l k n o w na r t i f i c i a li n t e l l i g e n c ep r o b l e m ，i e ，t h es t e a m r o l l e r p r o b l e m ，i ss u c c e s s f u l l ys o l v e db y i t ， t h ec o n c e p to f s u b s u m p t i o na n dt h es u b s u m p t i o nt e s ta l g o r i t h mn o to n l yc a ni n c r e a s e d e d u c t i o ne f f i c i e n c yb u ta l s op l a ya ni m p o r t a n tr o l ei nt h ef o r m a lm e t h o d sf o rs o f t w a r e e n g i n e e r i n g t h en o n e q u i v a l e n c eb e t w e e nc l a u s e - i m p l i c a t i o na n dc l a u s e - s u b s u m p t i o ni s p o i n t e do u ta n d as u f f i c i e n tc o n d i t i o nf o rt h e p r o p o s i t i o n “c l a u s eci m p l i e sc l a u s ed ，t h e nc s u b s u m e sd ”i sp r o p o s e da n d p r o v e d i ti sb r i e f l yd i s c u s s e dt oa p p l y t h em a n y - s o r t e dl o g i c w i t hr l dt og o f l w a r ec o m p o n e n t r e p r e s e n t a t i o na n d r e t r i e v a l f u z z ys e t s a n df u z z yl o g i ch a v eb e e np l a y i n ga n i m p o r t a n tr o l e i n d e a l i n gw i t h u n c e r t a i n t ya n dv a g u e n e s s i nr e a lw o r l d i ti sa n i m p o r t a n tr e s e a r c h d i r e c t i o ni nt h e a u t o m a t e dr e a s o n i n gc o m m u n i t yt oi n c r e a s et h e r e a s o n i n ge f f i c i e n c yb yu s i n gs p e c i a l r e l a t i o n sb e t w e e nd o m a i n e l e m e n t s s i m i l a r i t yi sa ni m p o r t a n tr e l a t i o ni nf u z z ys e t s w h e n e q u a l i t yc o n s t r a i n tc a n n o tb es a t i s f i e d ，s i m i l a r i t yc o n s t r a i n ti sap r o p e rc a n d i d a t ef o rt h e r e l a x a t i o no f e q u a l i t yc o n s t r a i n t s i m i l a r i t yh a sb e e nw i d e l ye x p l o i t e di na n yc o n t e x tw h e r e aw e a k e n i n go ft h ee q u a l i t yc o n s t r a i n ti su s e f u l ，s u c ha sa p p r o x i m a t e r e a s o n i n g t h e r e f o r e ， i i i i ti sv a l u a b l et oe x t e n dc l a s s i c a le q u a l i t yr e l a t i o nt of u z z yl o g i c ，i no r d e rt oi n t e g r a t et h e s i m i l a r i t yr e l a t i o ni n t of u z z yl o g i c ，s i m i l a r i t yi sr e g a r d e da s af u z z ye q u a l i t ya n daf u z z y l o g i cw i t hs i m i l a r i t yi sp r o p o s e d a n di t ss y n t a xa n ds e m a n t i c sa r eg i v e n p a r a m o d u l a t i o ni sa ni m p o r t a n ta n dap r a c t i c a li n f e r e n c er u l et od e a lw i t he q u a l i t y r e l a t i o ni nm e c h a n i c a lt h e o r e mp r o v i n g ，t h ep a r a m o d u l a t i o nr u l ei se x t e n d e dt ot h ef u z z y p r e d i c a t ec a l c u l u sa n dt h er e s o l u t i o n - a n dp a r a m o d u l a t i o n b a s e da p p r o x i m a t er e a s o n i n gi s d i s c u s s e d t h es i g n i f i c a n c eo f f u z z yl o g i c a li n f e r e n c eb y t h er e s o l u t i o na n dp a r a m o d u l a t i o n i sd i s c u s s e di ti ss h o w nt h a tf o ras e tso fc l a u s e si nf u z z y1 0 9 i cw i t hs i m i l a r i t y , i fe a c h c l a u s ei nsh a st r o t h v a l u em o r et h a n0 5 ，t h e ne v e r yc l a u s ei n f e r r e df o r msu s i n gr e s o l u t i o n a n d o rp a r a m o d u l a t i o ni ss i g n i f i c a n t c o n s i d e r i n gm a n y p r o b l e m s o l v i n gs y s t e m s a r eb a s e d o ns o c a l l e dr e d u c t i oa da b s u r d u m ，t h ec o m p l e t e n e s so f t h er e s o l u t i o na n dp a r a m o d u l a t i o ni s p r o v e d f o rf u z z y p r e d i c a t e c a l c u l u s ， a ni m p o r t a n ti s s u ei nt h ea u t o m a t e d r e a s o n i n gc o m m u n i t yi s t h ee v a l u a t i o no f a u t o m a t e dr e a s o n i n gs y s t e m si no r d e rt od e v e l o pm o r ep o w e r f u ls y s t e m sw i t h i nt h es a m e r e s o u r c el i m i t s t oi m p a r t i a l l ye v a l u a t ea u t o m a t e dr e a s o n i n gs y s t e m s ，a ni m p o r t a n tc r i t e r i o n i st h ep r o b l e m sr e p r e s e n t a t i o n t h e r e f o r e ，i ti sn e c e s s a r yt op r o v i d ea u t o m a t e dr e a s o n i n g s y s t e m sw i t ha u n i f o r mr e p r e s e n t a t i o nf o r m a t i no r d e rt op r o p o s et h ea u t o m a t e dr e a s o n i n g c o m m u n i t yw i t ha u n i f o r mf o r m a to f k n o w l e d g ea n dp r o b l e m sr e p r e s e n t a t i o no n t h ew e b ，a m a n y - s o r t e dk n o w l e d g em a r k u pl a n g u a g e ( a b b r m s k m l ) i sp r o p o s e d c o m p a r e dw i t h e x i s t i n gk n o w l e d g em a r k u pl a n g u a g e s ，t h em s k m l h a v et h ef o l l o w i n ga d v a n t a g e s ：o no n e h a n d ，t h en a m e so fe l e m e n t sc o r r e s p o n d t ot h e c o n c e p t s o fr e s o l u t i o n p r i n c i p l e a n d m a n y - s o r t e dl o g i c t h e r e f o r e ，a u t o m a t e dr e a s o n i n gc o m m u n i t y c a nb eq u i c k l yf a m i l i a rw i t h t h em s k m l f u r t h e r m o r e ，a p r o c e d u r em a y b ew r i t t e nt oa u t o m a t i c a l l yt r a n s f o r mt h es e to f c l a u s e sa n dr e f u t a t i o nt oam s k m lf i l e o nt h eo t h e rh a n d ，t h em s k m lc a n r e p r e s e n t n o t o n l y c l a s s i c a ll o g i c - b a s e dk n o w l e d g eb u ta l s om a n y s o r t e dl o g i c - b a s e do n e f o rm a n yu s e r s ，t h e ym a yh a v en os u f f i c i e n t k n o w l e d g et od e v e l o pa na u t o m a t e d r e a s o n i n gs y s t e m ，b u tt h e ya c t u a l l yn e e d t h es y s t e mt of u l f i l lt h e i rr e q u i r e m e n t s i nt h i sc a s e ， t h ea u t o m a t e d r e a s o n i n gs y s t e m s l o c a t e di nt h ei n t e r n e ta r ei m p o r t a n tr e s o u r c e sa n dc a nb e r e u s e db yw e bu s e r s t h a ti s ，t h ea u t o m a t e dr e a s o n i n gs y s t e m sc a n p r o v i d ew e b u s e r sw i t h a u t o m a t e dr e a s o n i n gw e bs e r v i c e s i ti sa l s ov a l u a b l ef o ra u t o m a t e dr e a s o n i n gs y s t e m s e v a l u a t i o nt op r o v i d ew e bu s e r sw i t ha u t o m a t e d r e a s o n i n gw e b s e r v i c e s ：w e bu s e r sc a nt e s t t h o s es y s t e m si np e r s o na n dd r a wt h e i ro w ne v a l u a t i o nc o n c l u s i o na b o u tt h o s es y s t e m s i n o r d e rt o p r o v i d e w e bu s e r sw i t ha u t o m a t e d r e a s o n i n gw e bs e r v i c e ap r o t o t y p e o f m a n y s o r t e dl o g i cw i t hr l d i si m p l e m e n t e d t h es y s t e mu s e st h es o a p ( s i m p l eo b j e c t a c c e s sp r o t o c 0 1 ) a st h ec o m m u n i c a t i o n p r o t o c o lb e t w e e nt h es y s t e ma n dw e bc l i e n t s ，a n d t h ea u t o m a t e dr e a s o n i n gw e bs e r v i c ep r o v e r s e r v i c ep r o v i d e db yt h es y s t e mi sd e s c r i b e d u s i n g t h ew s d l ( w e bs e r v i c e d e s c r i p t i o nl a n g u a g e ) k e y w o r d s ：a r t i f i c i a li n t e l l i g e n c e a u t o m a t e d r e a s o n i n g f u z z yl o g i c r e s o l u t i o np r i n c i p l e 胁6s e r v i c e v p r e d i c a t ec a l c u l u s k n o w l e d g em a r k u p 独创性声明 y 5 7 8 9 8 0 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除文中已经标明引用的内容外，本论文不包含任何其他个人或集体 己经发表过或撰写过的研究成果。对本文的研究作出贡献的个人和集体，均已在文中 以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：王家兵 日期：2 0 0 3 年9 月9 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：学校有权保 留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本 人授权华中科技大学可以将本学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 本论文属于不保密。 学位论文作者签名：王家兵 日期：2 0 0 3 年9 月9 日 指导教师签名：王能超 日期：2 0 0 3 年9 月9 日 采棼忭肴、导师弼意 匆垒丈公布 1 1 本文的研究目的 1绪论 本文的研究目的在于； ( 1 ) 自动推理是人工智能研究的核心内容，同时也是计算机科学与技术诸多子学科 的理论基础。本文试图通过对一阶逻辑、模糊逻辑的研究，在前人工作的基础上探索 新的自动推理原理与方法； ( 2 ) i n t e r a c t 的快速发展给人工智能提供了前所未有的发展机遇，同时也提出了新 的挑战。i n t e r a c t 环境下的知识表示与自动推理是人工智能研究者面临的新课题，本文 试图通过这方面的研究，提出i n t e m e t 环境下的基于逻辑的知识标记语言及构造提供 自动推理w e b 服务的自动推理系统。 1 2 选题的背景、研究目标及研究意义 1 2 1 选题的背景 自动推理( a u t o m a t e dr e a s o n i n g ) 是一门在给定知识及有关推理策略的前提下， 研究用计算机帮助人们进行推理的学科。自动推理的理论和技术是演绎数据库、硬件 验证、软件规约与验证、程序综合、专家系统、智能主体、智能机器人等研究领域的 重要基础。 1 2 1 1 人工智能的诞生 人工智能【2 4j ( a r t i f i c i a li n t e l l i g e n c e ，简称a i ) 是研究机器智能的学科，即用人工 的方法和技术，研制智能机器或智能系统来模仿、延伸和扩展人的智能，实现某些“机 器思维”。自动定理证明( a u t o m a t e d t h e o r e m p r o v i n g ，简称a t p ) 是自动推理领域中 的先驱性工作，也几乎是早期人工智能的代名词。 自动定理证明在3 0 0 多年前就成了人们追求的梦想。德国著名数学家l e i b u n i z ( 1 6 4 6 1 7 1 6 ) 第一个提出数学机械化思想的数学家提出利用一套数学符号 来刻划各种逻辑关系，建立一个“推理机器”，使得逻辑推导的工作变成一个纯粹的机 械化过程。这个梦想激励着优秀的科学家们，在几百年中做着不屈不挠的努力，直到 近代人工智能的诞生。 1 9 5 6 年的夏天，时在d a r t m o u t h 学院的j m c c a r t h 说服m l m i n s k y 、n l o c h e s t e r 及c s h a n n o n 把对自动机理论、神经网络及智能研究感兴趣的美国研究人员邀请到 d a r t m o u t h 来开一个研讨会。这次研讨会共有十人到会，包括m m 公司的t m o r e 和 a l s a m u e l 、麻省理工学院的o s e l f r i d g e 和r s o l o m o n f f 以及兰德公司和卡内基一 梅隆大学的a n e w e l l 、h a s i m o n 。为时2 个月的这次研讨会在学术思想上并没有取 得什么实质性的突破，但最后大家一致同意采用“a r t i f i c i a li n t e l l i g e n c e ”由m c c a r t h 提出的新名词来概括上述领域的研究方向，并从此宣告了“人工智能”这一新学 科的诞生。 1 2 1 2 人工智能的理论基础逻辑 逻辑与代数是计算机科学与技术学科的两大理论基础，是计算机科学的灵魂【1 ，“”。 从程序形式语义学、程序设计语言、程序规范理论到程序验证，从数据库理论、知识 库理论、智能系统到机器人的研究，所有的领域都与逻辑学存在着某种联系【”。逻辑 在计算机科学中的作用就好比数学在传统工程学科中所扮演的角色一样，是计算机科 学与技术这座大厦得以构建的最重要的基石之一。正如计算机软件设计大师、计算机 图灵奖获得者e wd i k s t r a 的肺腑之言【9 】：“我现在年纪大了，搞了这么多年软件，错 误不知犯了多少，现在觉悟了。我想，假如我早年在数理逻辑上好好下功夫的话，我 就不会犯这么多的错误。不少东西逻辑学家早就说了，可我不知道。要是我能年轻2 0 岁的话，就要回去学逻辑。”我国著名数理逻辑学家莫绍揆教授则更加直截了当d 0 ： “电子计算机与数理逻辑具有非常密切的关系。正是在数理逻辑中，把人类的推理过 程分解成一些非常简单原始的、非常机械的动作，才使得用机器代替人类推理的设想 有了实现的可能。事实上，它们( 程序设计) 或者就是数理逻辑，或者是用计算 机语言书写的数理逻辑，或者是数理逻辑在计算机上的应用。” 逻辑方法一直是计算机科学，特别是人工智能研究中的主要形式工具，之所以如 此，其根源可以追溯到计算机科学和逻辑学所追求的目标在深层次上的一致性【5 1 。从 本质上说，计算机科学就是要用计算机来模拟人脑的功能和行为，使计算机成为人脑 的延伸。而对于人脑的行为和功能的模拟，实质上就是模拟人的思维过程。正是计算 机科学所追求的这个目标，逻辑学这个研究人的思维规律和法则的学科，它的研究方 法和研究成果自然而然地成为计算机科学研究所选用的工具。 1 2 1 3 自动推理 l e i b u n i z 早在3 0 0 多年前就提出利用一套数学符号来刻划各种逻辑关系，建立一 个“雄理掇嚣”，使褥遥辍箍导翁工孬瓷或一个缝羚熬橇攘伍遗稳。磊寒德鏊蓑名数学 家d a v i d h i l b e r t ( 1 8 6 2 1 9 4 3 ) 则想得愆为大胆：他想建立一个“万能的”证明论( p r o o f t h e o r y ) 来一劳永逸地解决一切悬而未决的数学问题。 在2 0 邀纪的1 9 0 0 年，d ，h i l b e n 程巴黎国际数学家大会上徽了题为“数学闻题” 的著名演讲。h i l e b e n 在这次演讲中提蹬了纯认为在2 0 世纪必须解决静2 3 个数举难题。 其中最后一个问题是一个判定问题e n t s c h e i d l l i l 9 8 p r o b l e m ( d e c i s i o np r o b l e m ) ： 是否存在一个能够对任意有关自然数的命题给出真或假的判定的算法。 矮壤翔霆蠢题，弱递臻学懿术语趣蔽陈述是捂：绘定一个 薹惑熬请词逻褪公式翡 集合a 及任意一个谓词公式b ，是否存在一个算法，能对命题“b 是a 的逻辑结论” 给出“是”或“否”的回答。 h i l b e 戎摄出戆判定淘题是诱大载：懿粟存在个暹震戆判定冀法，那么就器。篷不 存在悬丽来决的问题了，因为所有的命题都将会被诞实或推翻；我们也不再需整所谓 的天才了，剿为任何一个判定问题都将由这个“力能的”判定算法来机械地给出证明 过程。 、 筵薏，许多铙秀静数理逻辑学家赣蓑这令方囊避行不潜逡努力【l “。在1 9 1 5 年 l e o p o l dl o w e n h e i m 与t l a r o a l ls k o l e m 同时首次研究了逻辑公式的满足性问题 ( s a t i s f i a b i l i t y p 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 l e m 的研究工作魂为后来的k u r t g 6 d e l 及j a c q u e s h e r b r a n d 的研究指明了方向。 在1 9 3 0 年k g 6 d e l 及j 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 t 及j h e r b r a n d 同时表明 了落谲演羹筑涯葫撬稳可以形式纯遗给爨任意一个逻辑寞懿命题瓣涯臻过程，莠都给 出了一个发现证明的构造性方法。谓词消算的完备性概念沟通了逻辑真的形式化可证 的语法属性与语义属性的联系。对于一个逻辑公式，精确的形式化语法与形式化语义 对逻辑真熬形式可涯性静磷变是霹等萋娶懿，然露在1 9 3 4 年鞋懿，这方嚣豹王掺主要 集中在形式化语法方面，糯没有涉及到形式化语义方丽。直到a 1 f r e dt a r s k i 在1 9 3 4 年 介绍了谓词演算的严格的形式化语义理论包括词+ 满足性、真德、逻辑结论及其它 有关概念的糖确定义以后，谓词演嚣理论2 j 。得以完善。 尽管在二卡篷纪二、三卡年代在臻调演算方蘑掰歌褥静上述戏采为后来鹃蕊予谓 词演算的定理证明及自动推理打下了坚实的理论基础，我们也可以说，上述成果对 h i l b e r t 所称的“证明论”而言是积极的成果，然而，在此期问传来的也不全是“好消 息”。 在1 9 3 1 年，数理逻辑学家k u r t g 6 d e l 提出了著名的不完备性定理( i n c o m p l e t e n e s s t h e o r e m ) ，该定理断言：即使在初等数论的范围内，对所有命题进行判定的算法也是 不存在的。 如果说g 6 d e l 的工作还只是从纯数学的角度回答了h i n e r t 的判定问题的话，那么 a l o n z oc h u r c h 与a l a nt u r i n g 的工作 1 2 - 1 3 对那些正在寻求一个能对任意一个问题给出 正确的“是”或“否”回答的证明程序的努力是一个巨大的打击。a l o n z oc h u r c h 与 a l a n t u r i n g 的工作表明，对于b 确实是a 的逻辑结论的情形，存在证明过程给出“是” 的结论；但如果b 不是a 的逻辑结论则不存在也不可能存在证明过程给出“否”的结 论。也就是说谓词逻辑是不可判定的( u n d e c i d a b l e ) 。 g 6 d e l 不完备性定理以及c h u r c h 与t u r i n g 的工作宣告了“万能推理机”幻想的破 灭。然而与悲观者只看到c h u r c h 与t u r i n g 工作的负面结果不同，乐观者同时也注意 到：尽管谓词逻辑是不可判定的，幸好，它还是半可判定的，即对于b 确实是a 的逻 辑结论的情形，存在证明过程给出“是”的结论。并且，尽管谓词逻辑是不可判定的， 但毕竟还存在着许多可判定的子类 1 4 - 1 6 。因此，人们关于机器定理证明与自动推理的 努力仍在继续。 就在1 9 5 6 年的d a r t m o u t h 研讨会上，n e w e l l 和s i m o n 提交了他们的一个自动推理 程序“逻辑理论家”( l o g i ct h e o r i s t ) ，“逻辑理论家”的目标是能够机械地模仿人类在 证明命题逻辑定理时所用的推导过程。在d a r t m o u t h 会议后不久，l t 就能够证明r u s s e l 与w h i t e h e a d 所著的数学原理( p r i n c i r l i am a t h e m a t i c a ) 第二章中的3 8 个定理。据 说r u s s e l 在s i m o n 给他演示这个程序发现了数学原理中一个定理的更为简洁的证 明以后非常高兴。在1 9 5 7 年，n e w e l l 、s h a w 和s i m o n 发表了他们有关这方面的成果， 这也是自动定理证明领域中发表的第一篇论文。他们所采用的方法也被称为启发式方 法( h e u r i s t i cm e t h o d ) 。 1 9 5 9 年g e l e r t e r 等人做出了几何定理证明机( g e o m e t r y t h e o r e mp r o v i n g m a c h i n e ， 简称g t m ) 。这个系统采用“反向链”的推理方法，亦即，从目标开始向前提产生新 的子目标，这些子目标逻辑蕴涵着最终目标。在g t m 产生的同时，出现了在逻辑e 建立定理证明器的第一次努力，即著名华人逻辑学家王浩和p - g i l m o r e 的研究工作。 他们的工作不同于n e w e l l 和s i m o n 的启发式方法，而是从经典逻辑的证明过程中总结 出推导规则，机械地去证明谓词演算中的定理。 王浩于1 9 5 8 1 9 6 0 年间研制出三个程序：第一个程序是关于命题演算的；第二个 程序是关于谓词演算中的可判定部分；1 9 5 9 1 9 6 0 年研制出的第三个程序是对整个谓 词演算的。其中第一个程序用3 7 分钟就证明了数学原理中的2 2 0 个定理j 。 以法国逻辑学家j a c q u e sh e r b r a n d 命名的h e r b r a n d 定理【l 8 在自动推理中扮演着至 关重要的角色。a b r a h a mr o b i n s o n 最先建议利用h e r b r a n d 定理来产生机械证明。 g i l m o r e 在1 9 6 0 年采用a r o b i n s o n 的建议写了一个程序【l ，这也是谓词演算的第一 个可用的机械证明程序。g i l m o r e 方法的理论基础是h e r b r a n d 定理，亦即，为了证明 谓词演算中某一个公式的恒假性，转化为去证明一个命题公式的恒假性。而证明一个 命题公式的恒假性时，g i l m o r e 采用了最原始的“乘法方法”。1 9 6 0 年，m a r t i nd a v i s 和h i l a r y p u t n a m 对g i l m o r e 方法作了改进，提出所谓的d p 算法【2 0 。在d a v i s 与p u t n a m 的程序中，介绍了子句形式，其基本思想是把变量用h e r b r a n d 域中的元素来替换以产 生基子旬来导致这些子旬的不完备性。p r a w i t z 在1 9 6 0 年提出了一个很重要的思想 2 i ： 让对命题不完备性的寻求来驱动搜索过程，只在必要的时候才从h e r b r a n d 域产生基项 以建立命题的不完备性。 在经过许多研究者的发展以后，这个思想终于导致了j a r o b i n s o n 在1 9 6 5 年提 出了著名的归结原理 2 2 1 ( r e s o l u t i o n p r i n c i p l e ) 。被r o b i n s o n 用归结原理所形式化的逻 辑里，没有公理，只有一条使用合一( u