（计算机软件与理论专业论文）基于广义归结的程序综合.pdf

火连理工人学硕士学位论文 摘要 自动程序设计是计算机科学中的重要研究领域，在人工智能的自动规划、机器人学 等分支有重要应用。在程序理论方面，程序综合与程序验证关系密切。程序综合就是从 定理机器证明中抽取程序，即：为构造一个符合给定输入输出规范( 通常表示为一组逻 辑公式，例如阶谓词公式) 的程序，首先把程序设计问题转化为定理证明问题，然后 从定理证明中抽取满足给定规范的程序。 对于形如( v i x 琴) 户仁，歹) 的定理证明j ；- i 题，广义归结原理可以回答其是否为真，而 对于“对每个确定的i 萝的值是什么? ”这一经典的证明论问题，广义归结原理本身 并没有给出解答。此前很多人研究从归结证明确定萝的值的方法，但是由于他们的方法 都不是从分析证明过程出发的，所以在很多情况下对问题的解不能做出很好的解释：只 能完成顺序问题的求解，或者只能列出问题的可能解，却不能回答在任意给定条件下问 题的解具体是什么。 这篇论文主要做了如下两项工作：第一，对于形如坼) ( 琴) p ( i ，歹) 的定理证明问 题，本文从分析广义归结证明树的每个结点入手，提取广义归结证明的过程信息，生成 问题求解程序。并且给出了所抽取出程序的部分正确性证明。这方法的特点是：抽取 算法所用的时间、空间复杂度与广义归结证明树包含结点数呈线性关系，并且抽取算法 本身十分简单，易于实现。第二，对于形如( w x 3 步x w ) p i ，歹，三) 的定理证明问题，广 义归结证明树中一般包含s k o l e m 函数，而从这样的广义归结证明树中抽取的程序就可 能包含s k o l e m 函数。本文给出了是否能够抽取出不包含s k o l e m 函数的程序的充分必要 条件，同时给出了消除s k o l e m 函数的算法。 本文给出的算法，主要适用于抽取顺序程序和分支程序，当定理是以递归形式给出 时，也可以抽取递归程序。利用数学归纳法，使用本算法可以抽取循环程序。 关键词：广义归结：广义归结证明树；定理证明；程序综合 基于广义归结的程序综合 p r o g r a ms y n t h e s i s b a s e do ng e n e r a lr e s o l u t i o n a b s t r a c t a u t o m a t i cp r o 群a m m i n gi sav e r ya c t i v ea r e ao fr e s e a r c hi nc o m p u t e rs c i e n c e i tp l a y sa n i m p o r t a n t r o l ei nf i e l do f p l a n n i n ga n dr o b o t si nt h er e a l mo f a r t i f i c i a li n t e l l i g e n c e i nt h e t h e o r y o f p m g r a m m i n g , p r o g r a ms y n t h e s i si sd e e p l yc o n c e r n e dw i t hp r o g r a mv e r i f i c a t i o n p r o g r a m s y n t h e s i se x t r a c t sp r o g r a mf r o mt h ea l i t o m a t e dt h e o r e mp r o v i n g t h a tm e a n s ，i no r d e rt o c o n s t r u c tap r o g r a ms a t i s f y i n gc e r t a i ns p e e i f i c a t i o m ( u s u a l l yr e p m s e n t e di nt h ef o r mo fa s e q u e n c eo fl o g i c a lf o r m u l a s ) ，at h e o r e mi n d u c e db yt h o s es p e c i f i c a t i o n si sp r o v e d ，a n dt h e d e s i r e d p r o g r a m i se x t r a c t e df r o mt h e p r o o f f o r t h e o r e m p r o v i n g p r o b l e ms u c h a s 怖胁) p g ，萝) ，t h e g e n e r a lr e s o l u t i o n p r i n c i p l e c a r l a n s w e rw h e t h e ri ti st r u eo rn o t , w h i l ef o rt h ec l a s s i c a lp r o o f t h e o r ya s f o re v e r yc e r t a i nx ，h o w t of i n dv a l u eo f y ? ：t h eg e n e r a lr e s o l u t i o np r i n c i p l ec a n n o tg i v et h ea i s w e rb yi t s e l f al o to f r e c e n tr e s e a r c hh a sc o n c e n t r a t e do nh o wt of i n dv a l u eo f _ yf r o mt h ep r o o ft r e s s w h i l e ， b e c a u s et h em e t h o d sa l en o tb a s e do nt h e a n a l y s i s o fp r o o fp r o c e d u r e ，t h e r ea r e m a n y l i m i t a t i o n si nt h e i rm e t h o d s f o re x a m p l e ，t h ef o r m e rm e t h o d s j u s tc a na n s w e rt h es e q u e n t i a l p r o b l e m ，o rj u s tc a nl i s t 棚t h ep o s s i b l ea n s w e r sw h i l ec a n n o tf i n dt h ea n s w e ru n d e rc e r t a i n c o n d i t i o n s i nt h i s p a p e r , t w op r o b l e m sa rs o l v e d f i r s t , f o r t h e o r e m p r o v i n gp r o b l e m s u c h a s ( w x 3 y ) m ，歹) ，w ep r e s e n t am e t h o d o f e x t r a c t i n gp m g a m f r o mt h ep r o o f g e n e r a t e d b y t h e g e n e r a lr e s o l u t i o np r i n c i p l e ，i tc o l l e c t sp r o c e s si n f o r m a t i o nf r o mt h eg e n e r a lr e s o l u t i o np r o o f t r e eb ya n a l y m g e v e r yn o d eo f g e n e r a lr e s o l u t i o np r o o f t r e e t oe x t r a c tp r o g r a m a n da l s o ，t h e p a r a a lc o r r e c t n e s so f t h ee x w a c t e dp r o g r a mi sp m v e d s e c o n d ，f o rt h e o r e mp r o v i n gp r o b l e m 吼励豁噼胁x v 三) p 仁，夕，牙) ，g e n e r a lr e s o l u t i o n p r o o f t r e e m u s ti n c l u d es k o l e m f u n c t i o n s ，s o t h ee ) ( t 嗡c t e dp r o g r a mf r o mt h i sk i n d o f p r o o f t r e em a y b e i n c l u d es k o l e mf u n c t i o n sa l s o i nt h i s p a p e r , a s u f f i c i e ma n dn e c e s s a r yc o n d i t i o ni s # y e nt oj u d g ew h e t h e rs k o l c mf u n c t i o n sc a nb e e l i m i n a t e df r o mt h ee x t r a c t e d p r ( w e a u r e o rn o t , a n dt h e e x t r a c t i n g m e t h o di sp u tf o r w a r d t h ea l g o r i t h mi nt h i sp a p e ri s a p p l i e dt oe x t r a c tt h es e q u e n t i a la n db r a n c hp r o g r a m i n a d d i t i o n t h em e t h o dc a ne x t r a c tt h er e c u r s i v ep m g r a mw h e nt h et h e o r e m su s e di np r o v i n ga r e i nt h er e c u r s i v ef o r m s ，a n da l s oc a ne x t r a c ti t e r a t i v ep r o g r a mb ym a t h e m a t i c a li n d u c t i o n k e y w o r d s ：g e n e r a lr e s o l u t i o np r i n c i p l e ；g e n e r a lr e s o l u t i o np r i n c i p l et r e e ；t h e o r e m p r o v i n g ；p r o g r a l ns y n t h e s i s i i 独创性说明 作者郑重声明：本硕士学位论文是我个人在导师指导下进行的研究工作 及取得研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文 中不包含其他人已经发表或撰写的研究成果，也不包含为获得大连理工大学 或者其他单位的学位或证书所使用过的材料。与我一同工作的同志对本研究 所做的贡献均已在论文中做了明确的说明并表示了谢意。 如芝理工大学硕士学位论文 1 1 论文的研究背景 计算机是新技术革命的一支主力，也是推动社会向现代化迈进的活跃因素。计算机 科学与技术是第二次世界大战以来发展最快、影响最为深远的新兴学科之一。计算机产 业已在世界范围内发展成为一种极富生命力的战略产业。 与此同时，随着社会信息化迅速发展，计算机应用越来越广泛，应用程序开发规模 越来越大，需求越来越多，软件系统日益复杂。目前软件生产正面临两个主要问题： 1 、由于开发周期过长，且需要长期维护，造成非标准化的软件生产开发成本过高。2 、 软件可信赖程度达不到实际要求。比如，t 9 9 7 年8 月i ( a l 的波音7 4 7 飞机撞山失事之 后，经调查发现，失事原因是客机坠毁时，关岛国际机场的雷达系统控制软件正出现故 障，未能在飞机接近地面时及时发出警报。1 9 9 6 年6 月4 日，阿丽亚娜5 型火箭第一 次鉴定发射，因火箭导航系统发生故障而失败。两次事故都可以归于软件设计问题。目 前，在安全要求极高的某些应用领域，计算机软件显然无法满足要求。更为严重的是， 随着软件复杂性提高和软件应用范围日益拓宽，上述两个问题日趋严重。 高度可靠的软件开发技术需要迅速、无误地完成大型应用软件系统。自从软件危机 出现以来，寻找类似可靠技术的努力从未终止。广义上，程序设计“1 被定义为基于不同 知识的推理过程，单靠人工完成，是不可能不存在错误的，因此，就需要对软件开发提 供机器支持，或开发基于知识处理和逻辑推理的软件工程工具。“。解决方法之一，就是 彻底摆脱目前的软件设计模式，用“做什么”型程序代替“如何做”型程序。这就涉及 到自动程序设计技术。自动程序设计是计算机科学中的重要研究领域，也是人工智能 追求的目标。 本文将讨论基于广义归结的程序综合方法。从广义归结证明树中抽取程序，解决对 于形如( 垤) ( 琴) p g ，力的定理证明问题。“对每个确定的夏。y 的值是什么? ”这一经 典的证明论问题。该方法对提高软件系统的正确性和可靠性，并提高软件开发效率有着 深远的意义和实际应用价值。 1 2 相关历史回顾及国内外研究现状 自动程序设计是指利用计算机自动地进行程序设计的活动。研究程序自动化有多种 不同途径。但经常涉及到定理证明和基于演绎推理的程序综合。因此。有必要对基于证 明的程序设计技术进行深入研究。 基于广义归结的程序综合 1 9 5 6 年，s i m o n 、n e w e l l 首先提出并讨论命题逻辑的机器推理系统，开辟了定理机 器证明领域。1 9 5 9 年，王浩在i b m 7 0 4 上实用类人法设计实现了3 个有效的定理机器证 明程序，引起国内外关注。1 9 6 5 年，r o b i n s o n 提出了处理子句形式公式集的归结方 法。由于归结方法推理规则简单，机器上容易实现，发展很快，至今仍是最有效的自动 推理方法之一。由w i l l i a mm a c u n e 完成的带支撑集策略的归结器o t t e r 有较多应用。 为了进一步提高归结推理的效率，很多学者对归结方法进行了研究，先后提出了锁 归结、语义归结、有序归结、线性归结、输入归结和单元归结等局部策略，以减少无用 子句的生成；还提出了包含删除策略，各种子旬化简策略等多种全局策略，尽可能多地 删除冗余子句。归结方法的另一发展是将其推广到非子句公式集。1 9 8 2 年，王湘洁、 刘叙华和m u r r a y 分别提出广义归结和n c - 归结。这两种方法很相似，都是以不含量词 的一般公式作为处理对象，且都是完备的。其中广义归结法，正是本文提出方法在定理 证明过程中采用的策略”1 。 在国内，定理的机器证明是人工智能领域主攻的课题。定理机器证明及其应用是我 国攀登计划项目之一。由于吴文俊先生在7 0 年代的杰出贡献，国内在几何定理机器证 明领域居于世界领先地位。实际上，定理机器证明研究领域的范围要广泛得多。在国外 更一般地叫做自动推理“。 此外，众多学者正在从事各类归结方法复杂度的研究“。“1 ，并试图通过研究各类归 结方法之间的关系，找到普遍适用的策略。虽然在最近，这种尝试已被证明是不可能成 功的“”，但在此过程中仍然产生了很多颇有价值的理论成果。 随着定理证明理论和实践的成熟，基于定理证明的程序综合方法“7 “1 的研究与开发 也飞速发展。该方法以公式作为程序规约，证明过程看作程序设计过程，并从证明中抽 取程序。也就是使用机器方法，综合那些可有效描述所需程序输入和输出之间关系的定 义信息。为构造一个满足定义信息要求的程序，程序综合需要证明：对任一有效输入对 象，都存在个有效输出对象。而在证明过程中，可以抽取所需的程序。8 0 年代初 m a n n a 深入研究了基于t a b l e a u 的演绎推理程序综合方法“4 ”。在这种方法中，将从规 格说明得到程序的过程看做一个定理证明的过程，通过利用规则重写、增加断言、合一 替换、归结以及数学归纳进行构造性证明。在构造性证明过程中。抽取证明的操作和中 间结果，构成程序的框架。 此后，程序综合方法策略的研究也迅速开展。”。 而本文研究的目的是研究基于广义归结证明的程序综合方法：通过从广义归结证明 树中抽取过程信息，实现自动程序设计。该方法可以提高软件开发效率，缩短开发周 期；利用更少的资源，解决更复杂的问题；并提高软件系统的正确性和可靠性。 2 大连理工大学硕士学位论文 1 3 本文的主要研究内容及内容组织 结合广义归结原理，定理机器证明和程序综合等技术，本文的主要研究内容是： ( 1 ) 利用广义归结原理的优势，设计利用广义归结原理，建立广义归结证明树的定 理机器证明方法。在此基础上建立的广义归结反演系统是用反演或矛盾的证明法，使用 广义归结推理规则建立的定理证明系统。 ( 2 ) 初步研究了试图降低广义归结原理时空间复杂度的几种策略。 ( 3 ) 对于形如i x 琴妒( i ，歹) 的定理证明问题，本文设计了新的从广义归结证明树 中抽取程序的方法：通过分析广义归结证明树中的结点，提取广义归结证明的过程信 息。生成的程序克服了以往的方法中的种种弊端，可以指出各种条件下，问题的解分别 是什么，从而不仅回答了“是什么”的问题。还能回答“怎样做”的问题。 ( 4 ) 给出了第三章提出的广义归结证明树抽取程序算法的部分正确性证明：若对任 意的输入五，p r o g 的输出为风，则一定有p ( 瓦，死) 为真。 ( 5 ) 为了能够顺利地从广义归结证明树中抽取出可用程序，须避免程序中含有意义 不明确的s k o l e m 函数。文中给出了是否能抽取出无s k o l e m 函数的程序的充分必要条 件，同时给出了抽取算法。 ( 6 ) 通过实例，解决不同类型的问题，解释本文阐述方法的应用。 论文的组织结构如下： 第一章：绪论部分，介绍了论文的研究背景，研究的目的和意义，国内外研究现 状以及本文的主要研究内容及内容组织。 第二章：预备知识，介绍了深入了解本文所需的一些知识准备，包括一阶谓词演 算的基本体系，归结原理和广义归结原理，国内外在从归结证明树抽取信息方向的研 究，以及从广义归结证明树抽取信息的概述。 第三章：详细阐述了本文所提出的从广义归结证明树抽取程序方法，并附有一个 实例。 第四章：给出了第三章提出的广义归结证明树抽取程序算法的部分正确性证明： 若对任意的输入瓦，p r o g 的输出为死，则一定有p ( x o ，y 。) 为真。 第五章：s k o l e m 函数的消除，给出了是否能抽取出无s k o l e m 函数的程序的充分 必要条件，同时给出了抽取算法。 第六章：应用举例。通过实例，解决不同类型的问题，从中可以很好的了解本文 提出方法的工作过程和相对于其他同类算法的优越性。 最后是本文的总结与展望，提出了需要改进的几个方面。 - 3 基于广义归结的程序综合 2 预备知识 2 1 1 概述 一阶谓词演算体系8 删首先规定有标点符号、括号、逻辑联结词、常量符号集、变 量符号集、h 元函数符号集、n 元谓词符号集、量词( 全称量词v 和存在量词丑) 等。 并根据这些规定，定义了谓词演算的合法表达式( 原子公式、合式公式) ，表达式的演 算化简方法，以便把一般化的表达式化成为标准式( 合取的前束范式或析取的前束范 式) 来讨论。化简结果的标准式记为： f s ( q l ) ( q 。x 。) m 其中国一) ( q 。矗) 为前束，代表各种量词的约束关系，肘称为母式，是不包含量 词符号量化的合式公式范式。 谓词演算中建立有很多推理规则，可用来从已知的公式集中推出新的公式，这些导 出的公式称为定理。给出定理的推理过程及所使用的推理规则序列就构成了该定理的一 个证明。在证明定理的演绎过程中，经常要对量化的表达式进行匹配操作，因而需要对 项作变量置换使表达式一致起来，这个过程称作合一。 2 1 2 标准式化简步骤 对任何一个合式公式可通过以下各步化成前束范式： ( 1 ) 消去多余的前束( 量词) 。这在化简过程都要随时注意到，因为可能出现母式中没 有其前束中相对应的约束变元，因而这个前束是多余的，应及时消去。 ( 2 ) 内移否定词的辖域范围。反复使用摩根律和量词互换式，把否定词移到只作用于原 子公式为止。 ( 3 ) 变量标准化。对变量作必要的换名，使每一量词只约束一个唯一的变量名。由于变 量名可任意设定，因而该过程不影响合式公式的真值。 ( 4 ) 把所有量词都集中到公式左面，移动时不要改变其相对顺序。 ( 5 ) 消去存在量词。对于待消去的存在量词，若不在任何全称量词辖域之内( 即它的左 边没有全称量词) ，则用s k o l e m 常量替代公式中存在量词约束的变量，若受全称量 词约束( 即左边有全称量词) ，则要用s k o l e m 函数( 即与全称量词约束变量有关的 函数) 替代存在量词约束的变量，然后就可消去存在量词。 4 大连理一大学硕士学位论文 例如公式 f = ( j x ) ( 砂) ( v z ) ( 了“) ( v v ) ( 3 w ) ( p ( x ，y ，2 ，”，v ，w ) 八( q ( 五y ，：，“，v ，们v r ( x ，z ，w ) ” 其中母式各变量中，四个存在量词所约束的变量应分别用如下所示的s k o l e m 函数和 常量替代； x = 口，y = b ，“= 厂( z ) ，w = g ( z ，v ) 消去存在量词后得 e = ( v z ) ( v v p ( 口，b ，z ，( z ) v ，g ( z ，v ) ) ( q ( 口，b ，z ，厂( z ) ，v ，g ( z ，v ) ) v r ( 口，z ，g ( z ，v ) ) ) ( 6 ) 把母式化成合取范式。反复使用结合律和分配律，将母式表达成合取范式的标准 型，最后得到一个s k o l e m 化的前束式f | 。 ( 7 ) 隐略去前束式。由于母式的变量均受量词的约束，可省略掉全称量词，但剩下的母 式仍假设其变量受全称量词量化。 ( 8 ) 把母式用子旬集表示。把母式中每一个合取元称为一个子旬，省去合取联结词，这 样就可把母式写成集合的形式表示，每一个元素就是一个子旬。如上例的子旬集 是： s = p ( a ，b ，2 ，( ：) ，v ，g ( z ，v ) ) ， q ( a ，b ，z ，厂( ：) ，v ，g ( z ，v ) ) v r ( a ，z ，g ( z ，i ，) ) ) ( 9 ) 子旬变量标准化。将子旬集中的变量作分离标准化，即对某些变量重新命名，使任 意两个予旬不会有相同的变量出现。由于每一个子句都对应一个不同的合取元，变 量都由全称量词量化，因而实质上两个子旬的变量之间不存在任何关系，变量标准 化不影响公式的真值。变量标准化这个步骤很重要，这是因为在使用子句集进行证 明推理过程，有时要实例化某一个全称量词量化的变量( 即用某一特定值替代变 量) ，这时就可能使公式尽量保持其一般化形式，增加了应用过程的灵活性。 2 1 3 标准式应用问题 经上述步骤化简得到的标准式是经过s k o l e m 化的前束范式，通常也称为s 一标准 形。要注意s 一标准形不是唯一的，若把它记为只，则只仅仅是f ( 未s k o l e m 化的前 束式) 的一个特例，取用不同的s k o l e m 函数会得到不同的结果。当，为非永假公式时， 只与f 并不等价，但当f 为永假时，只也一定是永假的，即s k o l e m 化并不影响f 的 永假特性。这个结论很重要，可用定理形式描述如下，它是下面将要讨论的广义归结原 理的主要依据。 5 基于广义归结的程序综合 定理：若s 是合式公式f 的s 一标准形之子旬集。则f 为永假的充要条件是s 为不 可满足的。 上面已经提到过子句的概念，它是s 一标准形母式中的合取元，因而每一个子句是 若干文字( 或基本式，即原子公式合原予公式否定式组成集合中的任一元素) 的析取 式。不含有文字的子句称为空子句。显然空子句是一种没有任何能满足某种解释的子 句，即空子句的取值总为假，一般简记为口或n i l 。个子句的文字中，其变量被常量 替代，就得到一个文字的基例，由基文字组成的子旬称基子句。 子句集中所有元素( 即子句) 的合取式不为真，卿j 称该予句集为不可满足的。 2 2 广义归结原理 2 2 1 广义归结原理概述 用1 9 6 5 年r o b i n s o n 提出的归结方法证明定理，要将定理的否定写成一阶逻辑中 的公式，再将公式化成s k o l e m 标准型，并将标准型的母式化成合取范式，合取范式中 的每一个项( 是一个析取式) 成为一个子句，于是合取范式对应着一个子旬集，归结方 法证明这个子句集是不可满足的，就相当于证明了该定理。 但是，将s k o l e m 标准型的母式化成合取范式，然后对子句集使用r o b i n s o n 的归结 方法，未必永远是最好的。 例如，关于群论的一个定理，其对应的子句集为 a ：e ( i ( x 1 x ，) 曰：p 【f ，x ，x ) c 卜p g ，y ， 卜p ( y ，z ，v p p 0 ，z ，w ) vp g ，v ，w ) d i p g ，y ，“卜一p ( y ，2 ，卜p b ，v ，w ) vp 0 ，z ，w ) e 卜p ( a ，f ，口) 其中c ，d 两式是由母式f ：v ( x ，y ，“) p ( y ，z ，v ) _ ( p ( “，z ，w ) 1 - 4v ( x ，v ，拆开 的，母式f 描述了群论中的结合律。显然，直接使用母式f 就更自然，更简便。 可以将母式f 看作一个广义子句，为此，王湘浩和刘叙华提出了广义归结方法 m 2 8 ，嚣】 经典归结方法把要证明的定理化为合取范式，范式化要大量使用分配律，从而使原 公式中文字的单次出现变为多次出现，形成冗余。此外，使用范式方法的推导由于去掉 了院名体重表达蕴含关系的连接词呻，演绎过程不自然。广义归结方法不必使用分 6 大连理工大学硕士学位论文 配律，而且可保留原命题的蕴含关系，使演绎过程更接近自然推导，明显优于经典归结 m 。 2 2 2 广义归结方法 在数理逻辑中，通常用丁与f 代表真与假，本文改用1 与0 。 定义设4 ，4 ，是一些原子，中( 4 ，a ：，4 ) 是以命题逻辑符号：，v ， ，斗，h 连 接这些原子和一些0 ，l 做成的公式，这样一个公式称为个广义予句。 定义如果一个广义子句中，没有原子出现，只由0 、1 、逻辑符号和括号组成， 则称此广义子句为常子句。特别，其值为0 的长子旬称为零子旬，其值为l 的长子句称 为壹子句。 设中“，鸣，4 ) 是一个广义予旬。在本文中特别注意巾中某些原子：4 。，4 时，可以把。写成m “，4 ) 。 例如，若特别注意4 时，可以将中“，4 ，4 ) 写成巾“) ，中( 4 = o ) 表示以0 代 中中4 的所有出现得到的广义子句。 以替换盯变中，可能合一4 与某些原子，中4 = o ) 表示在中4 中，以。代这些合 一后的所有出现得到的广义予旬。 定义设中“，4 ，a ) 是个广义子句，a i , ，a 是由中一些原子，其中，1 。 若4 ，4 ，有一个m g u ( 最一般合一替换) 盯，则m 。是合一4 ，4 ，所得到的的因 子。 定义设，t f 是两个广义子句，改名使无公共变量。设中4 是合一爿彳所得 到的中的因子。t f 是合一尽。，吃所得到的甲的因子。设p 是4 ，4b j 。7 的m g u ，于是： 巾”“9 = 0 ) v t f m 幢，= ) 酽匕”= 0 v a ”幢，v = 0 ) 都称为。与、壬，的广义归结式，其中4 ，骂，分别称为中、壬，中的归结原子。 定义设s 是一个广义子句集，巾是一个广义子句。从s 推出的d 的一个演绎是 一个有限广义子旬序列：i ，一，。， 其中( 1 ) o ，或者是s 中广义子句，或者是中。，o ：的广义归结式，k f ， 1 ) 。 设4 是m 的一个原子，令s = 枷l o s 由= m 0 = o ) ， 显然s 。不可满足，且s 1 种原子数小于n 。由归纳假设，存在从s 出发推出零子句的 演绎d 1 。在d l 。中初始结点上的s 中子句原来是a 的位置上再恢复，于是得从s 如发 的一个演绎d l ，而d l 演绎出的广义子旬，或是零子句，或是只含原子a 的广义子句 m ，且。似= o ) 是零子句。 若是前者，则归纳法完成。 若是后者，则令s ”= 舾”f o s m 0 = 1 ) = m “ ， 显然不可满足，且s ”种原子数小于n 。与上同理，存在由s 出发的一个演绎 d 2 ，而d 2 演绎出的广义子句，或为零子句，或为只含原子a 的广义子句甲，且 甲= = 1 ) 是零子句。 若是前者，则归纳法完成。 - 8 一 大连理工大学硕士学位论文 若是后者，则由m 与甲出发可得一个推出零子句的演绎d 1 ，因为与甲的广义归 结式：“= 0 ) v 甲i 一= 1 ) 是一个零子句。 将d 1 ，d 2 ，b 连接起来，得从s 出发推出零子句的演绎d ，归纳法完成。 充分性若存在从s 出发推出零子句的演绎d ，则s 不可满足。 若不然，设解释，满足s ，令演绎d 为如下广义子句序列：g i ，g2 ，一，q ，由演绎 的定义及命题1 知道，解释，满足每一个g 。( f _ 1 , 2 ，k ) 。特别，解释满足q 。但 是，g 。使零子句，矛盾。 关于提升引理叙述如下： 提升引理设中与、王，分别是广义子旬m 与甲的例，p 是o 。与甲的广义归结式， 于是，可取。与甲的广义归结式p ，使p 是p 的例。 定理2 ( 广义归结的完备性) 广义子句集s 不可满足，当且仅当由s 可逐步归结 出零子句。 证明必要性若s 不可满足，由h e r b r a n d 定理，则存在有限的不可满足的s 的基 例集f 。 由定理l 可知，存在从s 。出发推出零子旬的演绎d 。 将演绎树d i 中所有初始结点上的子句，都换成s 中的子句，并且使旧的子句是新 的子句的例，将每个非初始结点上的子句，也换成新子句，使新子句是其前任结点上新 子句的广义归结式，并且这些非初始结点上的旧子句也是新子旬的例( 由提升引理，这 是可以做到的) 。因为只有常子旬的例才是常子旬，特别，只有零子旬的例，才能是零 子句，故演绎树d 上的终点上的零子旬，仍然以零子旬代替。于是d 作如上修改后， 得到由s 推出的零子旬的演绎d 。 充分性的证明与定理1 相同，可略。 下面以一个简例说明谓词逻辑的广义归结过程。 例：已知：会朗读的人是识字的； 海豚都不识字； 有些海豚是很机灵的。 证明：有些很机灵的东西不会朗读。 首先把问题用谓词逻辑描述如下： 已知：( 协) ( r ( x ) 寸( x ) ) ( b k ) ( d ( _ 三( x ) ) 9 基于广义归结的程序综合 ( 3 x ) ( d ( x ) ，( x ) ) 再把前提条件的谓词公式进行化筒，将要证明的结论取反并化成广义予句型，求得 广义子句集： ( 1 ) r q ) o ) ( 2 ) d ( x ) _ ( x ) ( 3 ) d ( 彳) j ( j 4 ) ( 4 ) j ( z ) vr ( z ) ( 待证定理的否定形式) 从广义子句集求广义归结式，并将它加进广义子句集。连续进行直到产生零子句为 止。下面的广义归结式序列代表一个可行的证明过程： ( 5 ) 且( a )( 3 ) 和( 4 ) 的广义归结式 ( 6 ) 1 _ 工( 0 )( 5 ) 和( 1 ) 的广义归结式 ( 7 ) d ( 彳) 一0 ( 6 ) 和( 2 ) 的广义归结式 ( 8 ) 零予句( 7 ) 和( 3 ) 的广义归结式 2 2 3 广义归结证明树 从广义子句集s 出发，通过归结原理可得到一个向下的广义归结证明树。“，其每个 初始结点上附着一个s 中的广义子句，每个非初始结点上附着一个其前任结点上广义子 句的广义归结式。仍然引用上节的例子： 例广义子句集s = 仁( x ) _ + ( x ) ，d ( x ) 上( x ) ，d 似) ，( 彳) ，l ( z ) v r ( z ) ，演绎 过程如上节所示。此演绎可用下面的广义归结证明树表示，如图2 1 所示。 因此，广义归结证明树是关于广义归结证明的树的表示法，今后本文对广义归结证 明和广义归结证明树将不加区别的使用。称关于子句c 的广义归结证明树，是指子旬附 在根结点上的一个广义归结证明树。 此外，在实际问题求解中，为表示方便，本文在每条边上附加了可归结消去部分的 赋值信息；非叶结点下可附加其子结点的合一替换公式；非公理子旬结点外围用较粗的 黑线加以区分。具体方法后面有详细介绍。 - 1 0 犬连理工大学硕士学位论文 图2 1 广义归结证明树 f i g 2 1g e n e r a l r e s o l u t i o n p r o o f l r e e 2 2 a 降 匠广义归结方法复杂度策略 广义归结方法将一般谓词公式看作是一个广义归结式，将其看作是归结的基本单 位，因此使用广义归结方法可以使归结过程更自然、简洁。但如果广义归结过程时间和 空间复杂度过大，例如无法在一定时间内完成归结，便会阻碍了广义归结方法在实际中 的应用。因此，如何降低其算法复杂度，实际上是急待解决的问题。 t s e i t i n o ”给出了归结原理的复杂度下界，众多学者希望将此推广到广义归结，近 来，g o e r d t “”和其他研究成果表明这种尝试是不可能成功的。究竟这种尝试的不可能性 是否仅仅局限在某些个特定问题上，这个课题还在研究之中“8 。事实上，对于某个特定 问题，有的策略行之有效，另外一些策略表现很差；对于另外一个问题，则可能正好相 反。各种策略的分析及配合仍是有待解决的问题m 。 为使本文所提出的方法更具实用性，现根据前人成果，提出几个有助于降低广义归 结方法复杂度的策略。 ( 1 ) 降低时间复杂度方案： 研究证明宽度和证明长度之间的关系口3 ，对得到更为简化的证明过程有一定帮 助。 定义； w i d t h ：证明中任意予句所包含文字的最大数目。 s i z e ：一个推导的s i z e 为其中子句推导的行数。 b e ns a s s o n 通过研究证明宽度和证明长度之间的关系，指出，广义归结时应遵循如 下算法： 基于广义归结的程序综合 初始化i = l ： 由公理子旬开始，试图由所有最大宽度为i 的子句进行广义归结； 如果可以得到零子旬，广义归结结束。否则，i = i + 1 ，重新进行广义归结。 采取此方法进行广义归结，可以有效降低算法时间复杂度，本文中也借鉴了此种观 点和算法。 ( 2 1 降低空间复杂度方案。2 4 蚓： 单步证明方法 传统的定理机器证明系统的实现目标多为：将一个问题完全交给定理证明系 统，由定理证明系统自动给出证明。这样计算机面临的待选知识领域的规模非常庞 大，而且，很明显，这些知识的大部分对本问题证明无帮助。只有很小一部分知识 在证明过程中起作用，造成了巨大的空间浪费。 将一个定理证明表现为对若干个子问题的证明，而每一个子问题所涉及的知识 领域较小，从而使得每一个子问题的机器证明规模小型化，具有实际可行性。 通过部分逻辑谓词的真假值决定整个谓词公式的真假值 广义归结算法的目标就是尽早发现零子句，即逻辑结果为假的公式。根据某些 逻辑关系的定义，可以不求出整个公式中每一个谓词的真假值，再来决定公式的真 假值，而是通过一个( 或部分) 谓词的真假值来决定整个谓词公式的真假值。 这样可以提高整个广义归结的效率，因为，对于已经决定真假值的逻辑公式，其逻 辑公式中的谓词不再参与广义归结，也就是减少了参与广义归结的谓词的数量。 短谓词公式优先广义归结 尽早地确定一个谓词公式的真假值对提高广义归结效率是非常有帮助的。因 此，可以规定短谓词公式优先广义归结。虽然，广义归结前对谓词公式进行排序会 浪费了一定时间，但实践证明这是有必要的。 适当使用整体广义归结 如果参与广义归结的都是单个的原予，某些情况下，效率较低。可以将若干单 个原子视为一个整体进行归结。 避免重复公式进行广义归结 由广义归结的定义，如果参与广义归结的两个公式相同的，那么，归结到最后 将是一个壹子句，而不会所得到需要的零子句。因此应该尽量避免两个相同谓词公 式间的广义归结。 去除公式中冗余项 1 2 - k j g 理工大学硕士学位论文 2 3 从广义归结证明树抽取信息 上面部分介绍了广义归结原理，在此基础上建立的广义归结反演系统是用反演或矛 盾的证明法，使用广义归结推理规则建立的定理证明系统。它主要用来解决证明的问 题，即给定公式集r ，要求证明具有存在量词量化的目标公式( j x ) ( x ) 。但有时我们 希望能回答问题，即知道x 的某一个取值或x 的个例。对于直接回答x = a 时，w ( x ) 是否为宾这种问题，可直接用广义归结反演系统证明，即可给出结果。而对z = ? 时， v c ( a ) 为真的问题，则需要从广义归结证明中抽取信息来实现。 在以往的工作中比较有代表性的是g r e e n 的“回答谓词”方法“3 踟和l u c k h a m 的 “重言式”方法汹1 。 g r e e n 的方法是为待证定理加一个“回答谓词”，它的作用是收集归结证明用到的 替换。最终，回答谓词的参数反应了定理的解。他的方法主要应用在一些简单的问题求 解和程序综合问题上，但由于它的方法只适用于顺序程序，所以有很大的局限性。 l u e k h a m 的方法是为目标公式否定式的子句构造重言式；按照已找到的归结反演树 的结构，将目标否定式子句用永真式替代，每次归结、合一的文字集不变，生成出修改 证明树；根部子旬就作为所要提取的回答语句。应该说在许多时候，用l u c k h a m 的方法 得到的答案比用g r e e n 的方法得到的答案更具一般性，但由于这个方法并没有从分析归 结证明树的每个结点出发，所以，当得到的回答语句与目标公式有所不同的时候，未能 给出很好的解释，并且只能回答“是什么”的问题，不能解决“如何做”的问题。 本文论述的方法是从分析广义归结证明树中的每个结点入手，提取广义归结证明的 过程信息，从而生成程序，所以克服了以往的方法中的种种弊端：可以指出各种条件 下，问题的解分别是什么，从而不仅回答了“是什么”的问题，还能回答“怎样做”的 问题。并且由于抽取算法本身十分简单，所以有易于实现的优点。可以解决第一种推理 体系中的四类问题1 。 最后必须指出，抽取所得程序是由求得该程序的广义归结过程决定的。对于同一个 问题，可能存在几个不同的广义归结过程，这是由谓词演算的不可判定性决定的“，根 据每个过程，我们都能抽取一个程序。 - 1 3 基 寸“义归结的程序综合 3 从广义归结证明树抽取信息 一个广义归结证明树的每个结点都是广义子句集s 中的一个广义子句：表示公理、 已知定理的广义子句( 这两点在下文统称为公理子句) ，或者是待证定理否定后生成的 广义子句。而在广义归结证明树中，只有一部分结点可以抽取程序或程序片断，为此需 要下面定义： 定义1 ：将广义归结证明树中所有结点分为两类：公理结点和程序结点。 ( 1 ) 当结点为叶结点，如果结点表示公理子句，则称为公理结点：如果结点表示待 证定理否定后生成的广义子旬，则称为程序结点。 ( 2 ) 当结点为菲叶结点时，如果结点的两个子结点都是公理结点，则该结点称为公 理结点；否则称为程序结点。 与通常的广义归结证明树一样，每个结点都含有个广义予旬。此外，每个结点还 要附加上一个最一般的合一0 ，在叶结点处附加空替换，非叶结点处附加的替换就是生 成该广义归结式时所用的最一般的合一替换。这样，每个结点都呈( c 。，仃。) 的形式， c 是广义子句，盯，是合一替换，用下标来区分树中不同的结点。 本文介绍的抽取算法并不直接工作在上述证明树上，而是从变换后的证明树上抽取 程序，变换后的证明树与原来的证明树同构，具体定义如下。 定义2 ：设r o 是广义归结证明树，根结点是( o ，) ，按如下方法变换瓦： ( 1 ) 结点变为( o ，r o ) ，其中 g o = c r 0 ，即根结点保持不变； ( 2 ) 对于任意一个非根结点( c ，o i ) ，假设它的父结点已经变换为枷，f ，) ，则 ( c 。，q ) 变换为q 。，7 a 其中，d 。= 妒，t = 口，f 。 在变换后的证明树中，只含有常量和输入变量i ，是一种完全合一的证明树，故 称其为合一证明树，或简称合一树。以下用瓦表示广义归结证明树，其一般结点用 0 ，吼) 表示；用正表示合一证明树，其一般结点用心，r f ) 表示。 从广义归结证明树中抽取程序的方法如下： 记合一证明树为正，按如下方法从正中抽取程序： 按照从叶到根的次序给每个结点附加一段程序，最后附加到根结点处的程序即是从 归结证明树中抽取的程序。以下用p r o g ( d j ，f f ) 表示在结点 ，j ) 处的程序。 ( 1 ) 公理结点不附加程序。 一1 4 大连理工大学硕士学位论文 ( 2 ) 设叶结点( d ，r ) 是程序结点，f i = ( x 1 ，t