（课程与教学论专业论文）基于规则的平面几何双向推理系统.pdf

摘要 摘要 现有的几何自动推理系统采用较多的是基于单向推理法( 包括前向推理和后向推理) 的搜索方法。单向推理尤其是前向推理法已经取得了显著的成就，如z + z 智能教育平台的 系列软件平面几何、立体几何等就是基于前推法的自动推理系统。随着对平面几何 自动推理研究的不断深入，对推理效率提出了更高的要求。为了进一步提高平面几何自动 推理系统的效率，该文探讨了将前推法与后推法结合起来进行平面几何推理的方法。从该 系统的实际测试情况看，尤其是对较为复杂的几何问题，采用它可以显著提高推理效率。 文章首先对机器证明简史进行了回顾，然后对系统作了总体介绍，说明了谓词和规 则的选取。文中第三章是全文的核心部分，详细介绍了作者的工作思路。第节分析了各 种常见的推理策略及其优缺点，引出双向推理方法，并着重分析了后推的重点和难点、可 能遇到的问题以及解决办法；第二至六节对双向推理系统模型、工作过程等进行了描述 指出双向推理系统的程序主要包括三个类：信息类，引理类和推理类，其中推理类是整个 系统的核心程序。第七节介绍了对用户输入的可识别处理方法：第八节详细说明了几个关 键技术的实现等；第九节介绍了为提高推理效率所采用的一些方法。在第四章中作者对该 系统中的一些不完善之处及今后可能的改进做了简要的阐述和展望。附录给出了采用该系 统进行平面几何自动推理的一些例题。 关键词平面几何；自动推理；前向推理；双向推理；推理效率 a b s t r a c t a b s t r a c t t h ea u t o m a t i cr e a s o n i n gs y s t e mo fg e o m e t r ya p p l i e ss e a r c h i n gm e t h o d s w h i c ha r eb a s e d o nm o n o m i a lo n e si n c l u d i n gt h ef o r w a r dr e a s o n i n g a n dt h eb a c k w a r dr e a s o n i n g am o n o m i a l r e a s o n i n g ，e s p e c i a l l yt h ef o r w a r d r e a s o n i n gh a sm a d eg r e a ta c h i e v e m e n t s t h ep l a n eg e o m e t r y a n d t h e s o l i d g e o m e t r y , z + z s e r i e so f s o f t w a r eo f i n t e l l e c t u a le d u c a t i o n a lp l a t f o r m a i eb o t h b a s e d o nt h ef o r w a r dr e a s o n i n g w i t ht h e f t l r t h e r d e v e l o p i n g o fr e a s o n i n gs y s t e m ，t h eh i g h e r r e q u i r e m e n t sa r em a d e i nr e a s o n i n ge f f i c i e n c y s ot h ea r t i c l ew i l ld i s c u s so ni m p l e m e n t a t i o no f c o m b i n i n gt h ef o r w a r dr e a s o n i n g a n dt h eb a c k w a r dr e a s o n i n g f r o mt h ea c t u a le x p e r i m e n t a l r e s u l t ，t h i sw a y , e s p e c i a l l yi ns o m ec o m p l i c a t e dg e o m e t r y p r o b l e m ，c a l li m p r o v e t h er e a s o n i n g p r o d u c t i v i t y f i r s t ，t h e a r t i c l er e v i e w st h em a c h i n e r yd e m o n s t r a t i o n c h a p t e rt w om a k e s ag e n e r a l i n t r o d u c t i o no ft h es y s t e m i ti n t r o d u c e st h es e l e c t i o no fp r e d i c a t e sa n dr u l e s c h a p t e rt h r e e i s t h ec e n t e ra n di ti n t r o d u c e st h ew r i t e r st r a i no ft h o u g h t t h e f i r s ts e c t i o na n a l y s i ss e v e r a l c o m m o nr e a s o n i n gs t r a t e g i e sa n dt h e i re f f i c i e n c i e s ，i td r a w sf o r t ht h em i x e dr e a s o n i n ga n di t p u t se m p h a s i so n t h ek e y p o i n t sa n d d i f f i c u l to n e s ，t h ep o s s i b l eh a p p e n i n g sa n ds o l v i n gm e t h o d s - t h es e c o n ds e c t i o nt ot h es i x t hs e c t i o ni n t r o d u c et h em i x e dr e a s o n i n gs y s t e m sm o d e la n d w o r k i n gp r o c e d u r e ，a n dp o i n t so u t t h a tt h er e a s o n i n gs y s t e mi n c l u d e st h r e ec l a s s e sw h i c h a r et h e c i n f o ，t h ec l e m m a a n dt h ec r e a s o n i n g t h ec r e a s o n i n gc l a s si st h ec o r ep r o g r a m o f t h ew h o l e s y s t e m t h es e v e n t hs e c t i o ni n t r o d u c e sh o w t od ow i t ht h ek l s e r si n p u t ，s e c t i o ne i g h te x p l a i n s e x p l i c i t l yt h er e a l i z a t i o no f k e yt e c h n i q u e s s e c t i o n n i n ep r e s e n t ss o m em e t h o d st oi m p r o v et h e r e a s o n i n ge f f i c i e n c y i nc h a p t e r f o u r , t h ea u t h o rm a k e s ab r i e f e x p l a n a t i o na n dp r o s p e c to ns o m e i m p e r f e c tp l a c e sa n dp o s s i b l ei m p r o v e m e n t s i nt h ea p p e n d i x ，s o m ee x a m p l e s a r eg i v e no n c a r r y i n g o u tt w o d i m e n s i o n a lg e o m e t r ya u t o m a t i ci n f e r e n c ew i t h t h er e a s o n i n gs y s t e m k e yw o r d s t w o d i m e n s i o n a lg e o m e t r y ；a u t o m a t e dr e a s o n i n g ；f o r w a r dr e a s o n i n g ；m i x e d r e a s o n i n g ；r e a s o n i n ge f f i c i e n c y i i 广州大学学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指 导下，独立进行研究工作所取得的成果。除文中已经注明引 用的内容外，本论文不含任何其他个人或集体已经发表或撰 写过的作品成果。对本文的研究做出重要贡献的个人和集体， 均已在文中以明确方式标明。本人完全意识到本声明的法律 后果由本人承担。 学位论文作者签名：纰琵纱7 7 日期：卅年。月母日 广州大学学位论文版权使用授权书 本人授权广州大学有权保留并向国家有关部门或机构送 交论文的复印件和磁盘，允许论文被查阅和借阅。本人授权 广州大学可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇 编学位论文。( 保密的学位论文在解密后适用本授权书) 学位论文作者签名： 导师签名： 钕彻 铫，中 日期：p 吖年阳叫日 日期：刊年匕刖日 绪论 第一章绪论 1 几何定理机器证明研究概况 人工智能与自动推理技术的应用范围十分广泛，几何定理机器证明就是其中一个重 要的分支。 机器证明的发展经历了一个艰难的历程，历史上很多数学家曾在几何定理机器证明 这条道路上艰辛地探索过。为了用统一的方法处理千变万化的几何问题，笛卡尔 ( d e s c a r t e s ) 发明了坐标方法，创立了解析几何，这是科学史上的一件大事。在解析 几何的基础上，很多科学家对几何问题的机械化求解进行了研究。莱布尼兹( l e i b n i z ) ， 微积分的发明人之一，曾有过“推理机器”的设想，他还提出了现代计算机所采用的二 进制记数法。他的这些工作促进了数理逻辑早期研究的开展。跨1 9 世纪、2 0 世纪的大 数学家希尔伯特( h i l b e r t ) 在他的名著几何基础中，曾给出了一类几何问题的机 械化解题方法n “。 电子计算机的出现大大加快了数学机械化研究的进程，也促进了几何问题求解的机 械化研究。数学家们面临的一个基本的理论问题是，对于千变万化的几何问题，是否能 够纳入机械化处理的统一的轨道? 1 9 4 8 年，塔斯基( t a r s k i ) 发表了一条引人注目的定 理：“一切初等几何和初等代数命题构成的命题类，是可判定的”m ，。塔斯基定理的证明 是构造性的。也就是说，他确实提出了一套能判定任一个初等几何或初等代数命题的机 械化方法。他的方法是：先利用笛卡尔坐标将几何问题转化为代数问题，再用代数方法 来求解。遗憾的是该方法的计算复杂度太大，即使用高速计算机，也不能在合理的时间 内( 几小时或几天) 证明稍微复杂一点的几何定理( 如许多中学生就知道的西姆松定理 等) 。 沿着塔斯基的研究路线，发展出了几何问题机器证明的代数方法。1 9 7 5 年，考林斯 ( c o l l i n s ) 提出“柱面代数分解方法”，比塔斯基方法的效率提高了很多，但在计算机 上仍只能解决个别的稍微难点的几何问题。笛卡尔塔斯基考林斯，这是用代数 方法寻求几何问题机械求解的一条发展路线，。另一条路线是试图把解决几何问题的传 统综合方法机械化。这条路线是在1 9 5 9 年格兰特( g e l e r n t e r ) 发表的文章中首先提出 的1 。他设想的是从结论出发进行搜索，后来被称作后推链方法。1 9 7 5 年，奈文斯( n e i v i n s a j ) 又提出了更有效的前推搜索法m 1 ，这类方法又常被称作逻辑方法，或称人工智能 方法。该方法的优点是能产生出传统风格的证明，但由于搜索空间过大等问题，当时未 绪论 能形成有效的算法。 在几何问题求解机械化研究艰辛探索的2 0 多年间，数学机械化的研究和应用在总 体上有了长足的进步。计算机原先是只能进行数值计算的，到了2 0 世纪6 0 年代，计算 机也能作符号计算了，如进行有理式的四则运算、多项式的因式分解、求最小公倍式和 最大公因式等，甚至还能计算符号微积分。强有力的数学软件被开发出来，并在学校和 科技工作者中广泛应用“”。 数学机械化发展的有利环境，促进了几何解题机械化研究的突破。这项重要的突破 来自中国。1 9 7 7 年，我国著名的数学家吴文俊院士在中国科学杂志上发表了题为“初 等几何判定问题与机械化证明”的论文，提出了一个证明等式型初等几何定理的新的 代数方法。这个方法虽然不能证明几何不等式，但在证明等式型几何定理时效率比以前 的方法提高了很多。1 9 8 4 年，中国留美学者周咸青在他的博士论文中称该方法为“吴法”， 并列举了他基于吴法所编写的程序证明的1 3 0 个非平凡的几何定理。不久，他又在一本 专著中列出了用吴法证明的5 1 2 个几何定理。吴法从此在国际自动推理研究领域广为传 播，并使几何定理机器证明的代数方法的研究空前活跃起来，2 0 多年间就出现了好几种 成功的代数方法，包括目前应用较广泛的例证法等m 。 中科院院士张景中先生在机器证明的回顾与展望( 见参考文献 1 6 ) 文中指 出：“吴( 文俊) 法的成功使一度冷落的几何定理机器证明研究活跃起来，用代数方法 证明几何定理的方向受到重视，新的代数方法接连出现。用吴法可在微机上很快证 明困难的几何定理。这一进展是自动推理领域一大突破。被国际同行誉为革命性的 工作。”“代数方法不能使人满意的是，它所给出的证明是关于多项式的繁复的计算， 人难于理解其几何的意义，也难于检验其是否正确，能否让计算机生成人能理解和易于 检验的简明巧妙的证明，即所谓可读性证明。是对自动推理和人工智能领域的一个挑战 性课题。”1 9 9 2 年，张景中院士访问美国期间，将他从前提出的系统的面积解题方法 应用于机器证明的研究，使几何定理可读证明的自动生成这个难题得到突破。在与周成 青、高小山的合作研究中，发展了消点算法”1 ，并编制了程序，在n e x t 工作站上产生了 4 0 0 多条非平凡的几何定理的可读性证明1 ，从而使几何定理可读机器证明取得了突破 性进展。 1 2 智能教育软件研究现状 上世纪九十年代末期，随着家用电脑的日益普及，利用电脑进行辅助教学逐渐成为一 种趋势，在国内形成了广阔的软件市场，吸引了为数众多的商家和研究人员加入到教育软 绪论 件的研发行列。 目前教育软件市场虽然呈现出空前繁荣的状况，但是产品品质却良莠不齐，尤其是真 正高品质的智能教育软件较为稀少。一些软件企业过分注重开发成本，贪图眼前利益，其 产品只是将书本内容照搬上了电脑屏幕，再加上一些图像、声音等多媒体技术，充其量只 是课本的电子翻版或电子题库，根本无法在辅助教学中体现计算机快速、准确、信息量大 等优势，也无法利用计算机进行个性化教学。说到底，这种做法只是将知识由一种载体机 械地转移到另一种载体，软件开发者并没有太强的教育意识和对教育的研究。 当前教育软件的应用远远没有达到理想的效果，问题突出表现在：交互性不强、制作 欠精细、智能性欠佳等。随着智能技术、代理技术、虚拟现实技术、教育多主体技术等不 断发展，新一代的智能教育软件已经崭露头角。 由张景中院士提出的独具特色的“智能教育平台”的概念和理论，将自动推理理论应 用到智能教育软件的研究及其在教学的应用上，并进行了大量的教学实践。几年来，针对 教育需求，张景中院士带领研究人员开发了z + z 系列教育软件，包括平面几何n ，、解析几 何、立体几何“1 等学科的智能教育平台。这种新型的教育软件特色在于：与国内外常见 的多媒体课件开发平台不同，它能够从学科专业层面支持教学的全过程，而不仅是多媒体 编辑器：与题库、课件资源库不同，它所包含的学科内涵资源是即时生成的，并且提供 了资源加工和创作的工具，使教师和学生有广阔的发挥空问；与国外的数学解题软件、 几何作图软件不同，它能提供交互推理过程、逻辑动画生成、程序编写环境以及符号计算 等丰富功能“”。 将自动推理理论应用到教育软件已经成为当前一个重要的研究课题。该领域的研究将 为教育软件智能化开辟广阔的空间。 1 3 本文的工作 目前自动推理系统采用的推理方法主要有坐标法、几何不变量法和搜索法等。其中搜 索法是目前运用较多的一种推理方法“。其中基于前推的搜索法应用比较广泛，如z + z 智 能教育软件系列的平面几何，立体几何等就是采用的就是基于前推的搜索方法。 基于后推的方法也有应用，如由张景中院士等早年研究开发的几何专家m ，中的面积法 解题用的就是后推的方法。 基于前推的搜索法和基于后推的方法都各有其优缺点。前推法的优点是无论结论是否 能够推出都能根据已知的信息推理出大量有用信息，这一点对于启发学生思考有着十分重 要的意义；缺点在于扩展了许多与求解目标无关的信息，对比较复杂尤其是已知信息较多 绪论 的命题的推理而言，效率不够理想。后推法的优点是不必使用与目标无关的信息，目的性 强，同时还有利于向用户提供解释，适用于有大量己知信息而需要证明的目标又较少的情 况：缺点在于子目标的选择具有盲目性，求解了许多假目标，影响效率。 计算机解几何题模拟的是人类的思维方式，而人类求解问题往往是采用正向思维和逆 向思维相结合的方法进行，很少单独采取正向或逆向分析法。因此，研究如何实现一个将 前推和后推结合起来的双向推理系统，使它同时具有前推和后推的优点，对提高推理效率 和进一步优化推理过程是一个具有挑战意义的课题。基于对几何自动推理系统研究现状的 分析，笔者充分研究了前推系统和后推系统的优缺点，在导师的指导下完成了双向推理系 统的理论分析、建模、程序编写和实际测试工作。从实际测试的结果看，对较复杂尤其是 已知条件比较多的几何题目而言，采用双向推理系统对推理效率的提高是明显的。 本文第一章首先介绍了几何定理机器证明的发展简史，并对智能教育软件的研究现状 作了概述。 第二章介绍了双向推理系统的实现基础，包括谓词和规则的选择等。 第三章是全文的重点部分，介绍了双向推理系统模型、工作流程和系统结构，并分析 了系统实现的难点和重点，给出了一些关键技术的实现方法，包括予目标数据结构的设计、 子目标的生成、可读证明的产生等等。目前的平面几何自动推理系统采用的传统数据结构 虽然易于理解，但是往往容易引起几何信息的膨胀从而降低推理效率。为了进一步提高系 统的推理效率，本系统除了在推理方向上做了新的尝试外还实现了几何信息数据结构的优 化，提出了新的见解。另外，使用规则匹配的方法从已知信息不断组合产生新的信息，如 果信息量相当大，这个组合过程就难免产生组合爆炸，因此如何尽量避免规则匹配的重复 也是值得研究的。本章对系统采用的组合方法也作了介绍。 第四章通过实例比较对课题的研究成果作了简要介绍，经过比较与分析，最终得出的 结论是采用本系统的确能够提高推理效率和优化推理过程。 附录给出了采用本系统实现的部分几何题目。 1 4 本章小结 机器证明的发展经历了一个艰辛的探索过程，在中外很多科学家的不懈努力下，这 领域的研究取得了可喜的成果。智能教育是机器证明的实际应用领域之一，目前大多数教 育软件强调的只是多媒体在计算机辅助教学中的应用，离智能化相距甚远。在智能教育软 件研究方面，张景中院士的成果处于领先地位。目前几何自动推理系统采用的推理方法大 多是基于单向推理( 包括前向推理和后向推理) 的搜索方法，其中基于前推的搜索方法比 4 绪论 较常见。实际应用中这两种方法各有优缺点。笔者提出实现一个将前向和后向两种搜索法 结合起来进行推理的双向推理系统。 系统的实现基础 第二章系统的实现基础 2 1 e + + 语言的集合类 本系统是采用m i c r o s o f tv i s u a lc + + 6 o 开发完成的。v i s u a lc + + 是一种支持面向对 象的程序设计语言，可用于开发各类应用程序，功能十分强大，是目前最流行的程序设计 语言之一。面向对象的程序设计是一种围绕真实世界的概念来组织模型的程序设计方法， 它采用“对象”来描述问题空间的实体。 本系统使用了v i s u a lc + + 的集合类来定义几何信息的数据结构。集合类是用来容纳和 处理一组对象或标准数据类型变量的c 十十类。每个集合类对象可以看作一个单独的对象， 类成员函数可作用于集合的所有元素。m f c 提供两种类型的集合类：基于模板的集合类和 非基于模板的集合类。基于模板的集合类所包含的元素是用户自定义的数据结构或者说是 抽象的数据结构，它以数组、链表和映射表三种方式组织用户自定义的数据结构。使用基 于模板的集合类需要用户做一些类型转换工作。非基于模板的集合类提供的是一组现成 的、用于某种预定义的数据类型( 如c o b j e c t 、w o r d 、b y t e 、d w o r d 等) 的集合。在 设计程序时，如果所用的数据类型是预定义的，则使用非基于模扳的集合类；如果所用的 数据类型是用户自定义的数据结构，那就要使用基于模板的集合类。表2 - i 和表2 2 分别 列出了常用的非基于模板的类和基于模板的类【 1 。 根据对象在集合中的组织和存储方式，集合类又可分为三种类型：链表、数组、映射 ( 或字典) 。应当根据特定的编程问题，选择适当的类型。本系统使用的是数组类。 表2 1 常用的非基于模板的类 t a b l e2 - 1c l a s s e sn o n b a s e do n t e m p l a t ei nc o i t l r l l o nu s e 类名说明 c 0 b a r r a y动态可扩展c o b j e c t 指针数组 c p t r a r r a y动态可扩展v o i d 指针数组 c s t r i n g a r r a y动态可扩展c s t r i n g 对象数组 c o b l i s t c o b j e c t 指针双向链表 c p t r l is tv o i d 指针双向链表 c s t r i n g l i s tc s t r i n g 指针双向链表 c m a p s t r i n g t o o b以c s t r i n g 对象为关键字的c o b j e c t 指针映射 6 系统的实现基础 表2 - 2m f c 的基于模板的集合类 t a b l e2 - 2c l a s s e sb a s e do nt e m p l a t eo fm f c 类名说明 c a r r a y用于创建任何类型对象的数组 c l i s t用于创建任何类型对象的链表 c m a p用于创建任何类型对象的映射 c t y p e d p t r a r r a y用于创建c o b a r r a y 和c p t r a r r a y 对象安全类型数组 c t y p e d p t r l i s t用于创建c o b l i s t 和c p t r l i s t 对象安全类型链表 c t y p e d p t r m a p用于创建c o b m a p 和c p t r m a p 对象安全类型映射 数组类提供一个可动态调整数组大小的、有序的、按整数索引的对象数组。数组在内 存中连续的存放固定长度的数组元素。数组的最大优点是可以随时存取任一元素。数组类 包括基于模板的集合类与非基于模板的集合类。由于本系统用于描述几何对象的类是自定 义的数据结构，所以都使用基于模板的集合类。 数组的元素可以通过一个以零为基础的整数下标直接进行访问。下标操作符( 口) 可用 于设置或检取数组元素。如果要设置一个超过数组当前范围的元素，可以指定该数组自动 增大。如果不要求调整数组大小，则对数组集合的访问和对标准c 数组的访问一样快速。 但是如果需要调整数组大小，则数组占用的内存块需要重新移动，效率很低。在使用数组 之前，应使用s e t s i z e 0 建立其大小，并分配内存。若不用s e t s i z e 0 ，向数组添加元素 时会导致频繁的再分配内存和拷贝数据。因此说数组类适用于那些需要快速检索、很少需 要增加或删除元素的集合。 数组通过g e t a t ( 索引值) 来访问数组中的成员。要删除数组中的成员，可以用 r e m o v e a t ( k ) 删除数组的第k 个元素，然后再用d e l e t e 删除该指针指向的数据。 下面是系统中使用数组模板类的例子： 定义用于存放自定义类c i n f o 类对象的数组 c t y p e d p t r a r r a y c l n f o a r r a y ；c l n f o a r r a ym _ a r r a y ：定义数组 创建c l n f o 类对象i n f o c i n f o in f o = n e wc l n f o0 ： 将i n f o 加入数组 m a r r a y a d d ( i n f o ) ： 系统的实现基础 2 2 谓词和规则 2 2 1 谓词的选择 为了方便对采本系统进行描述，这里给出几个基本的定义。 定义2 1 几何图形中的点称为变元。 变元是构成几何命题的最基本的单位。在本系统中，所有的几何对象都可以用点来表 示。如线段a b 可以用两个点a 、b 表示，三角形a b c 可以用三个点a 、b 、c 表示等。 定义2 2 用一个或几个点来表示几何对象或几何特征，就称这几个点为一个点组。 如几何信息“三角形a b c ”、“a b c d 四点共圆”、“a b c 三点共线”等在本系统中都 是用点组表示的。单独的点是一个特殊的点组，只有一个变元。 说明：一个点组可以只含有一个变元，也可以有多个变元，但没有重复的变元。 定义2 ，3 规定几何构型中出现的若干个点之间的一种关系，称为谓词。 例如“中点”是涉及三个点的一种关系，可用谓词( m d p o i n t ) 表示，“平行”是 涉及四个点的一种关系，可用( p a r a l i e l ) 来表示等等。 谓词的选取应尽量能反映平面几何命题中的几何事实。谓词的多少直接影响系统的解 题能力。因此选取谓词的时候应当尽量丰富，但也不是越多越好。有些谓词会导致推理过 程中信息膨胀从而降低推理效率。表2 3 是本系统选取的部分谓词。 表2 3 谓词选取表 t a b l e2 - 3p r e d i c a t e ss e l e c t i o n 序号谓词示例意义 l m d p o i n t( m d p o i n tdab ) ：d 是线段a b 的中点 2 p a r a l l e l ( p a r a l l e labcd ) ：a b c d 3v e r t i c a l ( v e r t i c a labcd ) ： a b 上c d 4 s e g m e n t( s e g m e n tab ) ：线段a b 5 e q u a l o f s e g m e n t( e q u a l o f s e g m e n tabcd ) ： a b = c d 6 h a l f o f s e g m e n t( h a l f o f s e g m e n tabcd ) ： c d = 2 a b 7 a n g l e( a n g l eabd ) ： 么a b d 8 d o i n t s( p o i n t sa bc ) ：点a ，b ，c 9 e q u a l o f h n g l e( e q u a l o f a n g l eabcdef ) ：么a b c = 么d e f 系统的实现基础 续表2 - 3 序号谓词示例意义 1 0 t r i a n g l e _ 9 0 ( t r i a n g l e 一9 0 abc ) ：r t a b c 1 1 i s o t r i a n g l e( i s o _ t r i a n g l eabc ) ：等腰三角形a b c 1 2 e q u il t r i a n g l e( e q u i l _ t r j a n g l eabc ) ：等边三角形a b c 1 3c o n j r i a n g l e( c o n _ t r i a n g l eabcd ef ) ：a a b c 竺d e f 1 4o n l i n e( o n l i n eabc ) ：点a 、b 、c 共线 1 5r a t i o o f s e g m e n t ( r a t i o o f s e g m e n ta bc de fg h ) a b 术c d = e f 木g h 1 6i s ot r a d e( i s ot r a p eabcd ) ： 等腰梯形a b c d 1 7 p a r a l l e l o g r a m( p a r a l l e l o g r a mabcd ) ：平行四边形a b c d 1 8 r e c t a n g l e( r e c t a n g l eabco ) ：矩形a b c d 1 9 s q u a r e( s q u a r eabcd ) ：正方形a b c d 2 0r h o m b u s( r h o m b u sabcd ) ：菱形a b c d 2 1e c h e l o n( e c h e l o nabcd ) ：梯形a b c d 2 2h u b u a( h u b u aab cdef ) ：么a b c + d e f = 18 0 0 2 3h u y u a( h u y u aabcd ef ) ：么a b c + z d e f = 9 0 0 2 4s u m a a ( s u m a aldbc 一1adc1 8 0 ) ：么d b c + a d c = 1 8 0 0 2 5 5 u m s e g( s u m s e giab 一1cd 一1ef ) ： a b = c d + e f 2 6 s u m s q u r s e g( s u m s q u r s e gab c def ) ： 爿四2 = c r d 2 + e f 2 2 7 m d s e g m e n t( m d s e g m e n tab cd ) ：线段a b 、c d 互相平分 2 8m d v e r t i c a l( m d v e r t i c a lc dab ) ：c d 垂直平分a b 2 9 h a n g l e l i n e( h a n g l e l i n ed a bc ) ：肋是z a b c 的角平分线 3 0 r e s e m _ t r i a n g l e( r e s e m _ t r i a n g l eabcdef ) ：a b c a d e f 9 系统的实现基础 2 2 2 规则的表示与选择 定义2 4 通常的定义、公理、定理、公式等通称为规则。 前推规则可用符号表示为： i f t h e n 其中i f 语句部分确定了这条规则可以被采用的先决条件，t h e n 语句部分描述这条规 则所得出的结论。一般地说，如果一条前推规则被选用，就表示其前提条件已经被满足， 从而就可以对全局数据库进行操作使其发生变化，即应用这条规则后全局数据库由一种状 态变化为新的状态。由此可以看出，前推规则反映的是一个动态变化的过程。 后推规则可表示为： i f t h e n 其中i f 语句部分表示需要证明的结论，t h e n 语句部分描述的是使这个结论成立的条 件( 子目标) 。本系统中所编写的后推规则都是只有一个结论的，如果在推理过程中遇到 两个或者两个以上结论成立的情况，则使用递归、组队的方法找到其成立的所有可能条件。 这种方法在本文第三章有详细论述。 规则的多少是影响系统解题能力的关键因素。本系统的规则分为前推规则和后推规则 两种。前推规则包括了初中平面几何课本中的定义、公理、定理、公式。另有一些不属于 课本知识范围而属于常识的内容，也需要在规则中反映出来的。比如“两个角的值相等， 这两个角就是相等角”这个常识，如果不编写相应的规则，系统就无法掌握这个知识。后 推规则是一些常见几何信息的成立条件，包括了表2 3 中大部分谓词的成立条件。 2 3 测试系统介绍 本系统是在“几何推理实验研究系统( r e a s o n i n gt e s t ) ”基础上进行开发和测试的， 该平台具有直观、方便等特点。图2 一l 为该系统主界面。 双向推理系统的条件输入是在几何图形的作图过程中产生的。几何推理测试系统 ( g e o m e t r y ) 的作图系统有“智能作图”和“文本作图”两种方案，双方互为补充( 如图 2 2 ) 。 “智能作图”是直接使用鼠标在工作区定义点、直线等几何元素。该方法的优点是直 观、简便，并且易于将已知条件反映在图形上供推理使用。 “文本作图”采用命令方式定义几何元素( 如图2 3 ) ，如定义点a ( 2 0 0 ，3 0 0 ) 的一种 方法是采用坐标，命令行为p o i n t ( x ，y ，2 0 0 ，3 0 0 ) 。为了使文本作图方式更为简便，该系统 设置了文本命令作图对话框，用户无需记忆命令格式。 1 0 系统的实现基础 作图系统也有其局限性，有时不能将所有已知条件完全标注在图形上。对于这种情况， 系统提供了增加条件的对话框( 如图2 - 4 ) ，对作图时未能完全体现的条件进行补充。该对 话框同时也是定义所求结论的界面。图形、附加条件和“结论”构成了完整的几何命题。 图2 一l 几何推理实验研究系统( r e a s o n i n gt e s t ) 主界面 f i g u r e2 - im a i ni n t e r f a c eo fr e a s o n i n gt e s t 图2 - 2 作图系统 f i g u r e2 - 2m a i ni n t e r f a c eo fc o n s t r u c t i o ns y s t e m 1 l 系统的实现基础 图2 - 3 文本作图界面 图2 4 增加条件或结论界面 f i g u r e2 - 4i n t e r f a c eo fa d d i n gc o n d i t i o n so rc o n c l u s i o n s 2 4 本章小结 双向推理系统使用了v i s u a lc 十+ 的集合类来定义几何信息的数据结构。系统采用的是 基于规则的推理方法，谓词和规则的选择跟推理效率有着直接关系。系统采用。t 几何推理 实验研究系统( r e a s o n i n gt e s t ) ”作为开发和测试平台。 系统的实现 第三章系统的实现 3 1 常见推理策略分析 解数学问题，若从已知条件出发，运用已有的公理、定义和定理逐步推理，直至推出 结论，这种方法叫“综合法”。若从命题的结论出发，根据已知的定义、公理和定理逐步 寻找使该结论成立的条件，直至该结论成立的条件就是已知条件，这种方法叫做“分析法”。 对于比较复杂的数学问题，利用纯粹的综合法或分析法均很难解决问题，因此常常将分析 法与综合法结合起来使用。即一方面从已知条件入手，结合规则进行推理，得出一些结论； 另一方面从结论着眼，反向推理得出使该结论成立需要什么条件。二者相结合，最终找到 解决问题的途径。这种方法称为分析综合法。 同样，在进行推理系统设计时，也要考虑推理策略问题。1 3 提到过，目前初等几 何问题机器求解的常见的推理方法是搜索法，包括基于前向推理的搜索和基于后向推理的 搜索。 前向推理又称前推链、正向推理。用前推法搜索几何信息，其原始思想被称为“大英 博物馆”法，是一种古老的方法，它在几何定理机器证明中的应用，始于1 9 7 5 年m 1 ，1 9 9 6 年l o 月，张景中院士发表了题为基于前推法的几何信息搜索系统“”的论文，将前推 法这一古老的思想发展为有效的算法和程序，并第一次在几何自动推理中达到了不动点。 前推法的基本思想是从已知的信息出发，先匹配前提，再执行结论，不断产生新的事实， 逐步求解待解的问题。 后向推理又称后推链、逆向推理，将其应用在计算机证明几何定理领域是1 9 5 9 年提 出的m 。其基本思想是从目标出发，逆向搜索使目标成立的条件，将这些条件作为新的目 标，继续进行逆向搜索，直到所需要证明的目标可从己知信息库中找到。 双向推理又称正反向混合推理，是将前向推理与后向推理结合起来的一种推理方法。 从理论上说来，双向推理既克服了前推目的性不强和后推选择目标盲目的缺点，同时又结 合了两者的优点。具体的推理策略有多种，例如，通过数据驱动帮助选择某个目标，即从 初始证据( 事实) 出发进行正向推理，同时以目标驱动求解该目标，通过交替使用正逆向 混合推理对问题进行求解。双向推理的控制策略比单向推理策略复杂，美国斯坦福研究所 人工智能中心研制的基于规则的专家系统工具k a s ，就是采用正、逆向混合推理的产生式 系统的一个典型例子。 现有的初等几何自动解题软件基本都是基于单向推理方法的，应用较多的是前推搜索 方法。例如“z + z 智能教育平台平面几何”、“嘉科平面几何”等。前推法的优点是无 1 3 系统的实现 论是否能够推出结论，都能根据已知的信息推理出大量有用信息，这一点对于启发学生思 考有着十分重要的意义；缺点在于扩展了许多与求解目标无关的信息，对比较复杂尤其是 已知信息较多的命题的推理而言，效率不够理想。后推法的优点是不必使用与目标无关的 信息，目的性强，同时还有利于向用户提供解释，适用于有大量已知信息而需要证明的目 标又较少的情况；缺点在于子目标的选择具有盲目性，求解了许多假目标，影响效率m 。 鉴于单向推理系统的缺点，笔者考虑将双向推理方法应用于平面几何的自动推理，从而综 合单向推理系统的优点，克服其缺点。该方法目前在平面几何自动推理领域尚未得到有效 的应用。 这里用一个锥形图( 图31 ) 形象地比较基于单向推理的搜索方法和基于双向推理的 搜索方法，由该示意图可以看出，基于双向推理的搜索过程所扩展的信息数要比单向搜索 过程所扩展的信息数少很多。 图3 ，l 采用前后推结合的推理方法对信息扩展的影响 f i g u r e 3 1t h ei n f l u e n c eo ni n f o r m a t i o nn u m b e r sw h i l ea d o p t i n gm i x e dr e a s o n i n gm e t h o d 3 2 系统模型 本系统实现的双向推理方法是前推一轮与后推一轮交替进行，并在原始信息和目标的 某个中间结论上结合起来。其基本思想是：首先根据已知事实进行前向推理，然后从目标 出发进行后向推理，接着检查由前向推理所得的中间结论是否能够满足后向推理对于证据 的要求，如果满足则成功终止，否则继续下一轮推理，直到将这两种推理在已知事实和目 系统的实现 标之间某个中间环节上“接合”起来。图3 - 2 为系统模型示意图。 图3 - 2 双向推理系统示意模型 f i g u r e3 - 2s k e t c hm a po ft h em i x e d r e a s o n i l l gs y s t e m 3 3 系统流程图 图3 - 3 双向推理系统流程图 f i g u r e3 - 3f l o w c h a r to f b e m i x e d r e a s o n i n gs y s t e m 系统的实现 3 4 系统工作过程 i 通过入机界面向系统提交任务； 2 将外部信息转化为计算机内部信息； 3 。进行推理 ( 1 ) 前向推理产生新事实，向已知事实库中添加这个事实。添加时先检查有无相同的 信息，没有则添加，有则删除，这里包括对角、线段、平行的处理和等价类的应用； ( 2 ) 调用f i n d l n f o 函数判断事实库中有没有包含结论，如包含则转到第4 步； ( 3 ) 后向推理，产生相应的子目标，添加到子目标库中，添加时先检查有无相同的信 息，没有则添加，有则删除； ( 4 ) 调用c h e o k f b 函数判断子目标库中有无子目标被满足，如果有条件被满足则转到 第4 步； ( 5 ) 当双向推理达到不动点，推理失败，退出。 4 问题得到解决，根据已知事实库和子目标库生成问题的解答； 5 将内部信息表达形式转换为可读形式输出。 3 5 推理过程的c + + 描述 v o i dc r e a s o n i n g ：p r o o f ( c i n f o a r r a y c o n c l u s i o n ，8 0 0 lb h a s c o n ，b o o lb o n c e ) f i n to i d c o u n t ：i n tm n u m = o ： i n t n l e m m a g o u n t = m _ l e m m a g e t s i z e0 ： 将结论放入等价条件表中开始第一轮推理 i f ( mc o n c l u