（课程与教学论专业论文）基于前向推理的平面解析几何自动推理系统.pdf

摘要 摘要 几何定理机器证明的研究在最近2 0 年来取得了一系列令人瞩目的成果，特别是 计算机自动推理可读证明的突破，使几何定理机器证明的研究成果进入实用阶段， 应用于中学教学，成为计算机辅助教学的有力工具。其中以“z + z 智能教育平台” 系列的平面几何、立体几何等为代表的智能教育软件在同类软件中独树一 帜。该系列的特色之一自动推理，能在一个合理的时间内，对大多数的几何命题给 出符合人们阅读习惯的传统证明过程，受到了广大中小学教师和学生的欢迎，开辟 了几何定理机器证明新的应用领域。 在前人的工作中，平面几何的自动推理系统已经得到比较完善的实现，但是对 于平面解析几何的自动推理系统，目前还少有人涉及。本文在继承前辈工作成果的 基础上，采用了传统的前向推理策略，使用了代数方法和几何方法相结合的推理方 法，把解方程作为其核心思想，较完善的实现了这个平面解析几何的自动推理系统。 本文分五章： 第一章是绪论。简要介绍了计算机自动推理的历史和发展，自动推理在当前教 育软件方面的应用，并说明了本文的工作。 第二章对系统作了总体介绍，说明了谓词和规则的选取。 第三章是全文的核心部分，详细介绍了作者的工作思路，本系统的推理思想及 具体方法，对推理系统模型、工作过程等进行了描述，指出基于前向推理的平面解 析几何自动推理系统的程序主要包括三个类：信息类、推理规则类和推理类，其中 推理类是整个系统的核心程序。最后一节用实际例子分析了具体推理过程。 第四章继续用一些实例分析了推理系统的工作过程，说明了系统对于一些关键 问题采用的处理技术。 第五章是结论部分，给出了本文工作的意义及今后的工作方向。 最后以附录的形式列出了与本文内容相关的几何例子。 关键词：自动推理；解析几何；前向推理；解方程；谓词 a b s t r a c t i nt h ef i e l do fm a c h i n ep r o v i n gf o rg e o m e t r yt h e o r e m s ，p e o p l eh a v em a d eg r e a t a c h i e v e m e n t sd u r i n gt h ep a s t2 0y e a r s e s p e c i a l l ya f t e rt h eb r e a k t h r o u g ho fr e a d a b l e p r o v i n g f o r g e o m e t r yt h e o r e m s ，t h e f r u i t so f t h er e s e a r c ho nt h ep r o v i n gf o rt h eg e o m e t r y t h e o r e m sh a v eb e e n p u ti n t ou s e t h e y h a v eb e e nu s e di nt h es e c o n d a r ys c h o o le d u c a t i o n a n db e c o m ea l li m p o r t a n tt o o li nc o m p u t e ra i dt e a c h i n ga m o n gt h ev a r i o u se d u c a t i o n a l s o f t w a r e ，p l a n eg e o m e t r y a n ds o l i d g e o m e t r y , w h i c hb e l o n g t o “z + z i n t e l l i g e n t e d u c a t i o n a lp l a t f o r m ”，d e v e l o pi n t ot h e i ro w ns t y l e s ，o n eo fw h i c hi st h ea u t o m a t e d r e a s o n i n g p l a n eg e o m e t r ya n da 肼a l y a cg e o m e t r yc a ng i v ear e a d a b l e ，t r a d i t i o n a lp r o o f r e s u l ti nr e a s o n a b l et i m ef o ram a j o r i t yo f p r o b l e m so f t h em i d d l es c h o o lp l a ng e o m e t r y s ot h e yw e r eq u i t ew e l c o m et ot h es t u d e n t sa n dt h et e a c h e r s a u t o m a t e dr e a s o n i n gh a s e x p l o r e d an e w a p p l i c a t i o n f l d do f m a c h i n e p r o v i n gf o rg e o m e t r y t h e o r e m s i nt h ea n t e r i o rp e r s o n sw o r k , t h ea u t o m a t i c r e a s o n i n gs y s t e mo f p l a n eg e o m e t r y h a v e a l r e a d yg o t t h em o r e p e r f e c tr e a l i z a t i o n ，b u tt h ea u t o m a t i cr e a s o n i n gs y s t e m t ot h e p l a n ea n a l y t i cg e o m e t r y , r e t u r n i n g t h er a r ep e r s o nt oi n v o l v e c u r r e n t l y i ni n h e r i t i n gt h e f o u n d a t i o no f t h ee l d e rg e n e r a t i o nw o r k , t h i s p a p e r j u s t u s e st h et r a d i t i o n a lf o r w a r d r e a s o n i n gs t r a t e g y ，c o m b i n e st o g e t h e r t h ea l g e b r a r e a s o n i n gm e t h o d a n d g e o m e t r y r e a s o n i n gm e t h o d ，s o l v i n g t h ee q u a t i o nt ob ei t sc o r et h o u g h t ，c f l l r yo u tt h ea u t o m a t i c r e a s o n i n gs y s t e mo f p l a n ea n a l y t i cg e o m e t r yp e r f e c t l y t h e p a p e r i sd i v i d e di n t of i v ec h a p t e r s i n c h a p t e ro n e ，t h e a u t h o rr e v i e w s b r i e f l y t h e h i s t o r yd e v e l o p m e n t o ft h e a u t o m a t e dr e a s o n i n g ，i n t r o d u c e si t sa p p l i c a t i o nt oe d u c a t i o n a ls o f t w a r ea n dd e s c r i b e st h e a i mo f t h e p r e s e n ts t u d y i nc h a p t e rt w o ，t h ea u t h o rm a k e sa g e n e r a li n t r o d u c t i o no f t h es y s t e m ，i n t r o d u c e s t h es e l e c t i o no f p r e d i c a t e sa n dr u l e s t h ec h a p t e rt h r e ei st h ec e n t e ra n di ti m 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 ， i n t r o d u c e st h er e a s o n i n gs y s t e m sm o d e la n dw o r k i n g p r o c e d u r e ，a n dp o i n t so u t t h a tt h e r 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 ha r et h ec i n f o ，t h ec l e m m aa n dt h e c 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 mo ft h ew h o l es y s t e m t h el a s t t t t 些! ! ：竺! 一 _ 一一 s e c t i o na n a l y s e st h ei d i o g r a p h i cr e a s o n i n gp r o c e d u r eb y a c t u a le x a m p l e - l i lc h a p t e rf o u r ，t h ea u t h o ra n a | y s e st h er e a s o n i n gp r o c e d u r eb y s o m ea c t u a l e x a m p l eu n c e a s i n g i y ，i n t r o d u c e st h ed i s p o s a lt e c h n i q u et o s o m ep i v o t a lp r o b l e mo f t h e s y s t e m i nt h el a s tc h a p t e r ，c o n c l u s i o n sh a v eb e e nm a d e ，i n d i c a t i n gt h es i g n i f i c a n c eo f t h e t h e s i s a n ds o m es u g g e s t i o nf o rt h e f u t u r er e s e a r c hi sa l s og i v e n s o m e e x a m p l e s r e l a t e dt ot h i st h e t i sa r ep r e s e m e di nt h ea p p e n d i x k e y w o r d s ：a u t o m a t e dr e a s o n i n g ；a a n a l y t i cg e o m e t r y ；f o r w a r d r e a s o n i n g ； r e s o l v i n ge q u a t i o n ；p r e d i c a t e 广州大学学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指 导下，独立进行研究工作所取得的成果。除文中已经注明引 用的内容外，本论文不含任何其他个人或集体已经发表或撰 写过的作品成果。对本文的研究做出重要贡献的个人和集体， 均已在文中以明确方式标明。本人完全意识到本声明的法律 后果由本人承担。 学位论文作者签名：奄谤 曰期：上5 年s 月巧日 广州大学学位论文版权使用授权书 本人授权广州大学有权保留并向国家有关部门或机构送 交论文的复印件和磁盘，允许论文被查阅和借阅。本人授权 广州大学可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇 编学位论文。( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：毒滂 导师签霹州 日期：痧年5 月2 5 日 日期：o 礴易月、) 曰 广州大学硕士学位论文 第一章绪论 第一章绪论 1 1 几何定理机器证明研究概况 如何让计算机具有数学思维能力，亦即不仅会计算数学问题，而且能够证明数 学定理，这就是定理机器证明要研究的内容。这是十七世纪大数学家莱布尼兹 ( l e i b n i z ) 就开始幻想的课题。 人工智能与自动推理技术的应用十分广泛，几何定理机器证明就是其中一个重 要分支。 随着知识工程的迅速发展，大量定理机器证明方面的学者转向自动推理的研 究，这也扩大了定理机器证明的研究领域，即不再局限于数学领域，而是面对着整 个新一代计算机。因此，定理机器证明以及它派生出的自动推理的研究，是计算机 科学中的基本而重要的理论研究课题。 机器证明的发展经历了一个艰难的历程，历史上很多数学家曾在几何定理机器 证明这条路上艰辛的探索过。为了用统一的方法处理千交万化的几何问题，笛卡尔 ( d e s c a r t e s ) 发明了坐标方法，创立了解析几何，这是科学界的一件大事。在解析 几何的基础上，很多科学家对几何问题的机械求解进行了研究。莱布尼兹，微积分 的发明人之一，曾有过“推理机器”的设想，他还提出了现代计算机所采用的二进 制记数法。他的这些工作促进了数理逻辑早期研究的发展。跨1 9 世纪、2 0 世纪的 大数学家希尔伯特( h i l b e r t ) 在他的名著几何基础中，曾给出了一类几何问题 的机械化解题方法。 电子计算机的出现大大加快了数学机械化研究的进程，也促进了几何问题求解 的机械化研究。数学家们面临的一个基本的理论问题是，对于千变万化的几何问题， 是否能够纳入机械化处理的统一轨道? 1 9 4 8 年，塔斯基( t a r s k i ) 发表了一条引人 注目的定理：“一切初等几何和初等代数命题构成的命题类，是可判定的”。塔斯 基定理的证明是构造性的。也就是说，他确实提出了一套能判定任一个初等几何或 初等代数命题的机械化方法。他的方法是：先利用笛卡儿坐标讲几何问题转化为代 数问题，再用代数方法来求解。遗憾的是该方法的计算复杂度太大，即使用高速计 算机，也不能在合理的时间内( 几小时或几天) 证明稍微复杂一点的几何定理( 如 许多中学生就知道的西姆松定理等) 。 广州大学硕士学位论文 第一章绪论 沿着塔斯基的研究路线，发展出了几何问题机器证明的代数方法。1 9 7 5 年，考 林斯( c o l l i n s ) 提出“柱面代数分解方法”，比塔斯基方法的效率提高了很多， 但在计算机上仍只能解决个别的稍微难点的几何问题。笛卡尔一塔斯基一考林斯， 这是用代数方法寻求几何问题机械求解的条发展路线。 另一条路线是试图把解决几何问题的传统综合方法机械化。这条路线是在1 9 5 9 年格兰特( g e l e r n t e r ) 发表的文章中首先提出的| = = 3 。他设想的是从结论出发进行攫 索，后来被称作后推链方法。t 9 7 5 年，奈文斯( n e i v i n s h j ) 又提出了更有效的 前推搜索法汹3 ，这类方法又常被称作逻辑方法，或称人工智能方法。该方法的优点 是篚产生出传统风格的证明，但由于搜索空间过大等问题，当时未能形成有效的算 法。 在几何问题求解机械化研究艰辛探索的2 0 多年间，数学机械化的研究和应用 在总体上有了长足的进步。计算机原来是只能进行数值计算的，到了2 0 世纪6 0 年 代，计算机也能作符号计算了，如进行有理式的四则运算、多项式的因式分解、求 最小公倍式和最大公因式等，甚至还能计算符号微积分。强有力的数学软件被开发 出来，并在学校和科技工作者中广泛应用。 数学机械化发展的有利环境，促进了几何解题机械化研究的突破。这项重要的 突破来自中国。1 9 7 7 年，我国著名的数学家吴文俊院士在中国科学杂志上发表 了题为“初等几何判定问题与机械化证明“3 1 的论文，提出了一个证明等式型初等几 何定理的新的代数方法。这个方法虽然不能证明几何不等式，但在证明等式型几何 定理时效率比以前的方法高了很多。1 9 8 4 年，中国留美学者周成青在他的博士论文 中称该方法为“吴法”，并列举了他基于吴法所编写的程序证明的1 3 0 个非平凡的 几何定理。不久，他又在一本专著中列出了用吴法证明的5 1 2 个几何定理。吴法从 此在国际自动推理研究领域广为传播，并使几何定理机器证明的代数方法的研究空 前活跃起来，2 0 多年间就出现了好几种成功的代数方法，包括目前应用较广泛的例 证法等。 “吴( 文俊) 法的成功使度冷落的几何定理机器证明研究活跃起来，用代数 方法证明几何定理的方向受至重视，新的代数方法接连出现。用吴方法可在微机上 很快证明困难的几何定理。这一进展是自动推理领域的一大突破。被国际同行誉为 革命性的工作。”“代数方法不能使人满意的是，它所给出的证明是关于多项式的 繁复的计算，人难以理解其几何意义，也难于检验其是否正确，能否让计算机生成 广州大学硕士学位论文 第一章绪论 人能理解和易于检验的简明巧妙的证明，既所谓可读性证明，是对自动推理和人工 智能领域的一个挑战性课题。” 1 9 9 2 年，我国著名的数学家张景中院士访问美国期间，将他从前提出的系统的 面积解体方法应用于机器证明的研究，使几何定理机器可读证明的自动生成这个难 题得到突破。1 9 9 3 年，张景中院士和杨路、高小山、周咸青等人合作把消点法推广 到了非欧几何，用计算机发现了几十条非欧几何的新定理，并且自动生成了它们的 可读证明。 1 9 9 6 年后。李洪波博士、王东明博士发展了不变量方法，把消点法推广到了 广义的向量空间，即c l i f f o r d 代数。1 9 9 7 年，吉林大学的张树国教授和杨海圈博 士又把消点法推广，对一批关于圆锥曲线定理，用计算机自动生成了其可读证明。 1 9 9 9 年，在张景中院士的指导下，黄勇博士在其博士论文中完成了同一法的机器证 明，并编程实现了可视化推理。 几何问题，通常包括证明、计算、公式推导和作图。用消点法和几何信息搜索 系统做证明题、计算题和公式推导是方便的。几何作图又如何呢? 事实上，作图、证明、计算和公式推导是相通的。对一个作图题，假定图已经 作好了，再对图中的几何信息进行搜索推导，往往能发现作图的方法。这样，又开 辟了几何作图机械化的一条道路。 计算机自动生成几何问题可读解答的困难，被成功地突破了。 1 2 几何问题机器证明的几种主要推理方法 引用吴文俊先生的话总结几何问题机器证明的实质，就是“把质的困难转化为 量的复杂”3 ，这也是计算机自动推理算法思想的实质。 1 2 。1 基于坐标的代数方法 从d e s c a r t e s 到t a r s k i ，再到吴法，都是用代数方法机械来找几何问题的解。 吴法适用于证明“等式型”的几何定理，即可以将几何问题化为代数问题后，定 理的条件和结论都可以化为若干个多项式等式的形式。 文献1 指出，几何定理机器证明阔题可以分成下面两个主要步骤： 第一步，用解析几何方法建立坐标系设未知量，将条件表示成所设未知量的多 项式方程组g l ，将求证表示成多项式方程组g 2 ( 几何的代数化与坐标化) 。 广州大学硬士学位论文 第一章绪论 第二步，用一定算法( 如吴方法) 判断g 2 是否可以由g l 推出。 在吴法的影响下，相继出现了很多新的方法。周咸青提出用g r o b n e r 基方法来 构造几何定理机器证明的方法，洪加威提出的单点例证法。“，张景中、杨路提出的 数值并行法“，这些方法都实现了非平凡几何定理的机器证明。 利用代数的方法是利用多项式( 组) 来证明，所以生成的证明过程是复杂的， 是不可读的并且难于理解，但是对于特殊问题，如代数曲线、曲面的几何问题“还 需使用代数方法，其中的一个新进展是杨路研究员提出的实系数代数方程的完全判 别式系统。 1 2 2 基于几何不变量的消点法 基于坐标的代数方法只是对给定的题目判断其结论的正确与否，整个过程都是 多项式的运算。人们要想搞明白为什么结论正确，几乎是不可能的。在这样的背景 下，给出几何命题的让人能看懂的证明过程的问题被科学家多次提出。 1 9 9 2 年，中国科学院张景中院士应邀赴美国进行合作研究，他根据以前发展的 系统的面积解题方法“”“州，提出了几何定理机器证明的新方法，即基于几何不变 量的消点法，这里的几何不变量是面积，故常称为面积法。后来在这个基础上，李 洪波博士、杨海圈博士发展了不变量方法，用向量法来实现几何定理可读证明，即 c 1i f f o r d 代数o 。3 “。 1 2 3 基于综合证明的几何信息搜索系统 以面积法为代表的几何不变量法，尽管能给出一大类几何定理的通用证明方 法，但证明的过程不能够完全合乎人们通常的习惯，比如在证明中使用一些消点公 式等。1 9 5 9 年，g e l e r n t e r 发表的论文中提出一种解决几何问题的传统综合方法的 机械化3 。g e l e r n t e r 用的是从结论出发进行倒推推理的方法，通常叫做后推搜索 法。1 9 7 5 年，n e v i n s 又提出了更有效的前推搜索法，这种方法的最大优点是能产 生传统风格的证明，但未形成有效的算法。1 9 9 6 年，张景中、高小山、周咸青提出 一个基于前推模式设计的“几何信息搜索系统”( g i s s ) 。利用g i s s 系统编制的c 程序证明了1 6 1 个非平凡的几何命题。用这种方法搜索几何信息，其思想是“大英 4 广州大学硕士学位论文 第一章绪论 博物馆方法，利用已知信息推出所有的结论。显然，这种方法的瓶颈是几何信息 的膨胀。 1 3 智能教育软件研究现状 上世纪九十年代末期，随着家用电脑的日益普及，利用电脑进行辅助教学逐渐 成为一种趋势，在国内形成了广阔的软件市场，吸引了为数众多的商家和研究人员 加入到教育软件的研发行列。 目前教育软件市场虽然呈现出空前繁荣的状况，但是产品品质良莠不齐，尤其 是真正高品质的智能教育软件较为稀少。一些软件企业过分注重开发成本，贪图眼 前利益，其产品只是将书本内容照搬上了电脑屏幕，再加上一些图像、声音等多媒 体技术，充其量只是课本的电子翻版或电子题库，根本无法在辅助教学中体现计算 机快速、准确、信息量大等优势，也无法利用计算机进行个性化教学。说到底，这 种做法只是将知识由一种载体机械地转移到另一种载体，软件开发者并没有太强的 教育意识和对教育的研究。 当前教育软件的应用远远没有达到理想的效果，问题突出表现在：交互性不强、 制作欠精细、智能性差等。随着智能技术、代理技术、虚拟现实技术、教育多媒体 技术的不断发展，新一代的智能教育软件已经暂露头角。 由张景中院士提出的独具特色的“智能教育平台”的概念和理论，将自动推理 理论应用到智能教育软件的研究及其在教学的应用上，并进行了大量的教学实践。 几年来，针对教育需求，张景中院士带领李传中副研究员、黄勇博士等研究人员开 发了z + z 系列教育软件，包括平面几何。3 、解析几何。j 、立体几何。3 等学科的智能教 育平台。这种新型的教育软件特色在于： 与国内外常见的多媒体课件开发平台不同，它能够从学科专业层面支持教学的 全过程，而不仅是多媒体编辑器。 与题库、课件资源库不同，它所包含的学科内涵资源是即时生成的，并且提供 了资源加工和创作的工具，使教师和学生有广阔的发挥空间。 与园外的数学解题软件、几何作图软件不同，它能提供交互推理过程、逻辑动 画生成、程序编写环境以及符号计算等丰富功能。 将自动推理理论应用到教育软件已经成为当前一个重要的研究课题。该领域的 广州大学硕士学位论文第一章绪论 研究将为教育软件智能化开辟广阔的空间。 1 4 本文的工作 目前自动推理系统采用的推理方法主要有坐标法、几何不变量法和搜索法等。 其中搜索法是目前运用较多的一种推理方法。其中基于前推的搜索法应用比较广 泛，如z + z 智能教育软件系列的平面几何、立体几何等就是采用的基于前 推的搜索法。 几何定理机器证明的研究在七十年代已经取得突破，可读证明的实现也近十年 了，自动推理的软件也出现了很多，尤其平面几何方面的教育软件已经比较常见， 但是关于解析几何的自动推理系统在国内还不多见，笔者采用自动推理中常见的前 推搜索法尝试实现一个平面解析几何的自动推理系统，可以实现解析几何中一些常 见命题的自动推理和证明，其中也包括平面几何中的定理和命题，并且实现了推理 过程的可读输出。 本文第一章首先介绍了几何定理机器证明的发展简史，并对智能教育软件的研 究现状作了概述。 第二章介绍了平面解析几何自动推理系统的实现基础，包括谓词和规则的选择 等。 第三章和第四章是全文的重点部分，介绍了基于前向推理的平面解析几何自动 推理系统模型、工作流程和系统结构，并分析了系统实现的难点和重点，给出了推 理算法的c 十+ 代码实现，分析了推理采用的一些关键技术。通过一些实例介绍分析 了推理过程。 第五章通过实例对本课题的研究成果作了简要介绍，最终得出本系统在实现平 面解析几何的自动推理方面是比较有效的。 附录给出了采用本系统实现的部分平面解析几何题目。 为了简便起见。本文中凡是称解析几何的地方都是指平面解析几何。 1 5 本章小结 几何定理机器证明的发展经历了一个艰辛的探索过程，在中外很多科学家的不 懈努力下，这一领域的研究取得了可喜的成果。智能教育是机器证明的实际应用领 6 广州大学硕士学位论文 第一章绪论 域之一，目前大多数教育软件强调的只是多媒体在计算机辅助教学中的应用，离智 能化相距甚远。在智能教育软件研究方面，张景中院士的研究成果处于领先地位。 目前解析几何的推理系统在国内还不多见，笔者采用了常见的前向推理搜索方法尝 试实现了一个平面解析几何的自动推理系统。 广州大学硕士学位论文 第二章系统实现的基础 第二章系统实现的基础 2 1 c + + 语言的集合类 本系统是采用m i c r o s o f tv i s u a lc + + 6 0 开发完成的。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 - 1 和表2 - 2 分别列出了常用的非基于模板 的类和基于模板的类。 根据对象在集合中的组织和存储方式，集合类又可分为三种类型：链表、数组、 映射( 或字典) 。应当根据特定的编程问题，选择适当的类型。本系统使用的是链 表类。 表2 - i常用的非基于模扳的类 t a bio2 1cl - s 暑8n o n b a s e do nl ：e m pi _ t eino o l l l m o nu s 6 类名说明 c o h a r r a y动态可扩展c 0 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 tc o b l e c t 指针双向链表 c p t r l i s 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 指针映射 广州大学硬士学位论文 第二章系统实现的基础 链表类提供一个可动态扩展的对象链表。链表在内存中是不连续存放的，链表 的最大优点是可以随时对任一元素进行操作而不需要移动其他元素的位置。链表类 包括基于模板的集合类与非基于模板的集合类。由于本系统用于描述几何对象的类 是自定义的数据结构，所以都使用基于模板的集合类。 表2 吨常用的基于模板的集合类 t a b i e2 2c i a s s e sb a s e do nt e m p i a t ei nc o m m o nu s e 类名说明 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 对象安全类型映射 链表的元素可以通过链表的指针域逐次进行访问，访问链表中的某一个元素可 能需要访闯这个元素之前的所有元素，所以对链表元素的访问不如数组那样方便。 但是链表一般不受存储空间的限制，向链表中增加一个元素，链表可以自动扩展， 当需要调整链表大小时，链表占用的内存块不需要重新移动，效率很高。在使用链 表之前，不需要事先分配内存大小，向链表中添加元素不会导致频繁的再分配内存 和拷贝数据。因此链表类适用于那些需要频繁增加和删除元素、但是不需要快速检 索元素的集合。 链表类通过它的很多成员函数对它的成员进行操作，常用的成员函数包括 g e t h e a d ，r e m o v e h e a d ，g e t n e x t 等等。 下面是系统使用链表模板类的一个例子： t y p e d e fc t y p e d p t r l is t c d r a w o b j l is t ： c d r a w o b j l i s tmo b j e c t s ：对象集合 创建c i n f o 类对象i n f o c l n f o * i n f o - - n e wc l n f o 0 ： 将i n f o 加入链表 m _ o b j e c t s a d d t a i l ( i n f o ) ： 广州大学硕士学位论文 第二章系统实现的基础 2 2 谓词和规则 2 2 1 谓词的选择 为了方便对本系统进行描述，这里给出几个基本的定义。 定义2 1 几何图形中的点称为变元。 变元是构成几何命题的最基本的单位。在本系统中，所有的几何对象都可以用 点来表示。如线段a b 可以用两个点a 、b 表示，三角形r b c 可以用三个点a 、b 、c 表示等。 定义2 2 用一个或几个点来表示几何对象或几何特征，就称这几个点为一个 点组。 如几何信息“三角形a b c ”、“a b c d 四点共圆”、“a b c 三点共线”等在本系 统中都是用点组表示的。单独的点是一个特殊的点组，只有一个变元。 说明：一个点组可以只含有一个变元，也可以含有多个变元，但没有重复的变 元。平面解析几何中几何对象的属性和几何对象之间的关系构成谓词 定义2 3 平面解析几何中几何对象的属性和几何对象之间的关系构成谓词。 无论是在平面几何推理系统还是解析几何推理推理系统中，几何信息库中都以 “谓词”来区分各种不同的几何信息。谓词是规定几何构形中出现的若干个点之闻 的一种关系，如“两直线平行”、“线段中点”等。几何信息库中，将谓词相同的 信息放在一个集合里。在推理时，每条推理规则的条件是几何信息，利用信息的谓 词和信息在对应集合中的位置来定位每条信息。 例如“中点”是涉及三个点的一种关系，可用谓词( p r f m d p o i n t ) 表示，“平 行”是涉及四个点的一种关系，可用( p r f l i n e p a r a l l e l ) 来表示等等。 谓词的选取应尽量能反映几何命题中的几何事实，这一思想无论是在解析几何 还是平面几何中都是一致的。谓词的多少直接影响系统的解题能力。因此选取谓词 的时候应当尽量丰富，但也不是越多越好。有些谓词会导致推理过程中信息膨胀从 而降低推理效率。 因为解析几何与平面几何的图形表达方式不同，所以解析几何中的谓词选取与 平面几何中有所不同，这主要体现在表达几何关系的方式上有所不同。理论上平面 几何中有的谓词解析几何中全都有，而解析几何中有的谓词平面几何中不一定有， 解析几何中包括了平面几何中没有的谓词，如解析几何中表示变量、斜率，点与直 广州大学硕士学位论文 第二章系统实现的基础 线距离的谓词在平面几何中就不会有，表示椭圆、双曲线等二次曲线的谓词平面几 何中就更不会有。 在本系统中，所有的谓词都放在一个枚举变量中，用枚举变量来定义谓词可以 方便用数字序号来存储和引用谓词。 下面是本系统定义谓词的代码： 增加谓词修改此处 e n t l mp r e d i c a t i o n ( p r f v a r ，p r f l e n g t h ，p r f p o i n t ，p r f e q l s e g m e n t ，p r f o n l i n e ， p r f r a t i o ，p r f m d p o i n t ，p r f c o n c l i n e ， p r f t g c e n t r e ，p r f s e g m e n t r a t i o ， p r f e q u a t i o n ， p r f l i n e ，p r f l i n e s u p e r p o s i t i o n ， p r f l i n e p a r a l l e l ，p r f l i n e u p r i g h t n e s s ， p r f l i n e i n t e r s e c t h n g l e ，p r f l i n e i n t e r s e c t ， p r f p o i n t l i n e d i s t a n c e ，p r f l i n e d i s t a n c e ， p r f c i r c l e ，p r f l i n e c i r c l e t a n g e n c y ， p r f e l l i p s e ，p r f h y p e r b o l a ，p r f p a r a b o l a ， p r f o n c i r c l e ，p r f o n e l l i p s e ， p r f o n h y p e r b o l a ，p r f o n p a r a b o l a ， p r f c i r c l e c i r c l e t a n g e n c y ， p r f m o v e ，p r f p a r a m e t e r ，p r f p o l a r c o o r d i n a t e s ) ： 表2 - 3 对本系统选取的部分谓词作出一定解释。 2 2 2 规判的表示与选择 定义2 4 通常的定义、公理、定理、公式等通称为规则。 前推规则可用符号表示为： i f t h e n 其中i f 语言部分确定了这条规则可以被采用的先决条件，t h e n 语句部分描述这 型查兰堡主兰垡笙苎 兰三兰墨竺茎墨! ! 苎堕 表2 - 3 谓词选取表 序 谓词 示例 意义 号 1 p r f v a r( p r f v a ra ) ： a 是一个变量 2p r f l e n g t h ( p r f l e n g t hab ) 线段a b 长度 3 p f p o i n t( p r f p o i n ta ) 点a 4p r f e q l s e p e n t( p r f e q l s e g m e n tabcd ) 线段a b 和c d 相等 5 p r f o n l i n e( p r f o n l i n eabc )点a 在直线b c 上 6 p r f r a t i o( p r f r a t i o0a )圆o a 的半径 7p r 删d p o i n t( p r f m d p o i n tdab ) d 是线段a b 的中点 8 p r f c o n c l i n e( p r f c o n c l i n eabc )a ，b ，u = 息廷筏 9 p r f t g c e n t r e( p r f l g c e n t r eabc )三角形a b c 的重心 1 0p r f s e p e n t r a t i o( p r f s e g m e n t r a t i oabcd )线段a b 和c d 的长度日 1 l p r f e q u a t i o n 表示方程 1 2 p r f l i n e( p r f l i n el 1 )直线l 1 1 3p r f l i n e s u p e r p o s i t i o n( p r f l i n e s u p e r p o s i t i o nl 1l 2 ) 两直线l 1 l 2 重合 1 4 p r f l i n e p a r a l l e l( p r f l i n e p a r a l l e ll 1l 2 )两直线l 1 ，l 2 平行 1 5p r f l i n e u p r l g h t n e s s( p r f l i n e u p r i g h t n e s sl 1l 2 ) 两直线l 1 ，l 2 垂直 1 6p r f l i n e i n t e r s e c t a u g l e( p r f l i n e i n t e r s e c t a n g l el 1l 2 )两直线l 1 l 2 的夹角 1 7 p r f l i n e i n t e r 8 e c t ( p r f l i n e i n t e r s e c tl 1l 2 )两宜线l 1 ，l 2 相交 1 8 p r f p o i n t l i n e d i s t a n c e( p r f p o i n t l i n e d i s t a n c eal 1 )点a 与直线l 1 的距离 1 9 p r f l i n e d i s t a n c e( p r f l i n e d i s t a n c el 1l 2 )两直线l 1 l 2 的距离 2 0 p r f c i r c l e( p r f c i r c l e0a )圆o a 2 1p r f l i n e c i r c l e t a n g e n c y( p r f l i n e c i r c l e t a n g e n c yl 10a ) 直线l 1 与圆o a 相切 2 2p r f e l l i p s e( p r f e l l i p s ec o )椭圆c 0 2 3p r f e l = l y p e r b o l a( p r f i l y p e r b o l ah 0 ) 双曲线h o 2 4 p r f p a r a b o l a( p r f p a r a b o l ap o )抛物线p o 2 5 p r f o n c i r c l e( p r f o n c i r c l eb0 )点b 在圆0 a 上 2 6p r f o n e l l l p s e( p r f o n e l l l p s eac o )点a 在椭圆c o 上 2 7p r f o n h y p e r b o l a( p r f o n h y p e r b o l aah o )点a 在双益线h o 上 2 8 p r f o n p a r a b o l a( p r f o n p a r a b o l a p o )点a 在抛物线p 0 上 2 9p r f c i r c l e c i r c l e t a n g e n c y( p r f c i r c l e c i r c l e t a n g e n c ya bc d )两圆a b ，c d 相切 1 3 广州大学硕士学位论文 第二章系统实现的基础 条规则所得出的结论。一般地说，如果一条前推规则被选用，就表示其前提条件已 经被满足，从而就可以对全局数据库进行操作使其发生变化，即应用这