（课程与教学论专业论文）反证法在自动推理系统中的研究与实现.pdf

摘要 从5 0 年代t a r s k i 发表的初等代数与初等几何的判定问题【2 5 1 开始，到 7 0 年代的吴法1 4 5 】，9 0 年代的消点法【8 ，】0 1 ，几何定理机器证明的研究经历了几个 阶段的发展。 计算机技术的发展及可读机器证明的出现 3 ，4 1 ，使这个方向的研究成果进入 了实用阶段。以张景中院士为领导的小组在此基础上开发了一系列的智能教育软 件【”】。得到广大中小学教师，学生的欢迎。这些软件最突出的一个特点就是自 动推理。 要让计算机能够自动进行推理。首先要“教会”计算机推理的方法，计算 机“掌握”了方法后，才能进行推理。因此，“教会”计算机推理方法是首要的。 现行的推理软件都是采用了前推搜索的推理模式。从题目的己知条件出发， 利用规则进行推理直至推出所需要的结论。在数学证明方法上属于直接证明方 法。这种方法只能证明一些肯定性的命题。但对于一些否定性，唯一性的命题 采用直接证法不易证明，这就需要利用数学证明中的间接证明方法来证明。间接 证明方法中比较常见的一种方法是反证法。 尽管几何定理机器证明的研究在七十年代已经取得突破，可读证明的实现也 近十年了。但自动推理在反证法方面还存在很大的不足。除了在平面几何【2 2 l 中见到有间接证法中的同一法外，其他的教育软件中很少有实现反证法的。 本文的工作就是向这个方向努力的一个尝试，把数学证明中的反证法与机器 证明中的前推搜索法相结合。使计算机在自动推理方面能够更加完善。 本文共分为四章： 第一章，简要介绍自动推理的历史和发展，阐述本文要解决的问题。 第二章，介绍本文的工作原理及实现技术。 第三章，给出作者今后的工作方向。 第四章，给出本系统证明的些例题。 v 一j 丛幽型l 一 a b s t r a c t f r o mt l r s l ( i ，sn o t a b l ew o r k ad e c i s i o nm e t h o d f o re l e m e n t a r ya l g e b r aa n d g e o m e t r y i n1 9 5 0 st ot h e 19 7 0 s w u sm e t h o da n dt h e1 9 9 0 s p o i n t se l i m i n a t i o n m e t h o d t h ed e v e l o p m e n to f t h er e s e a r c ho f a u t o m a t e dr e a s o n i n g i ng e o m e t r yh a s e x p e r i e n c e d s e v e r a ls t e p s a st h ed e v e l o p m e n to fc o m p u t e rt e c h n o l o g ya n dt h ed i s c o v e r yo fr e a d a b l e p r o o f so nm a c h i n ep r o o f s ，t h er e s u l t si nt h i sf i e l dh a v eb e e np u ti n t ou s e t h eg r o u p w h i c hl e a db yz h a n gj i n g z h o n gh a v ed e v e l o p e das e r i e so fi n t e l l i g e n te d u c a t i o n a l s o f f w a r e s ，t h es o f t w a r ew e r ew e l c o m e d a st h e yf i r s tp u b l i s h e d ，t h em o s to u t s t a n d i n g c h a r a c t e r i s t i co f t h es o f t w a r ei st h ea u t o m a t i cr e a s o n i n g l e tt h ec o m p u t e ra b l et oc a l t yo nr e a s o n i n ga u t o m a t i c a l l y s h o u l d ”t e a c h t h e r e a s o n i n g m e t h o do f t h ec o m p u t e rf i r s t ，a f t e rt h ec o m p u t e rh a s ”g r a s p e d ”t h em e t h o d ， c o u l dc a r r yo nr e a s o n i n g s o ，i ti sp r i m a r yt o ”t e a c h ”t h er e a s o n i n gm e t h o do ft h e c o m p u t e r a tp r e s e n t , m o s ts o f t w a r eu s e df o r w a r dc h a i n f r o mt h ek n o w nc o n d i t i o n st o r e s u l t s w h i c hi sam e t h o do fd i r e c t l yp r o v i n g ，t h i sm e t h o do n l yp r o v es o m e a f f i r m a t i v ep r o p o s i t i o n s ，b u tt os o m en e g a t i v e ，s o l i t a r yp r o p o s i t i o n si sv e r yd i f f i c u l t t op r o v e w h i c hn e e di n d i r e c t l ym e t h o dt op r o v e ，t h ep r o o f b yc o n t r a d i c t i o ni so f t e n u s e di ni n d i r e c t l yp r o v i n g t h o u g ht h er e s e a r c ho fa u t o m a t e dr e a s o n i n gi ng e o m e t r yh a dg a i n e ds u c c e e d i n1 9 7 0 s ，t h e r ei sa l m o s tt e ny e a r ss i n c et h ed i s c o v e r yo fr e a d a b l ep r o o f ，b u tt h e a u t o m a t e d r e a s o n i n g i ss h o r to f i n d i r e c t l yp r o v ew e o n l y s e et h eu n i t e dm e t h o di n v i 叁i 苎照 ，t h e o t h e rs o f t w a r e sh a v en o ta c h i e v e dp r o o f b yc o n t r a d i c t i o n t h i s p a p e rg i v e sat r yo n t h i sf i e l d t om a k et h ea u t o m a t e d r e a s o n i n g i r l o r e p e r f e c t w em a k e t h ep r o o f b yc o n t r a d i c t i o nc o m b i n e i 也f o r w a r dc h a i n t h i sp a p e ri sd i v i d e di n t of o u rp a r t s c h a p t e ro n e ：i n t r o d u c i n gt h ea u t o m a t e dr e a s o n i n gh i s t o r ya n di t s d e v e l o p m e n t ，d e s c r i b i n gt h em a i na i mo ft h i sp a p e r c h a p t e rt w o ：i n t r o d u c i n gt h ep r i n c i p l eo nt h i sp a p e ra n dt h ed e t a i l s c h e m eo nt h i sp a p e r c h a p t e rt h r e e ：g i v i n gs o m eq u e s t i o n s ，a n dt h ed i r e c t i o no ft h ef u t u r e w o r ko ft h ea u t h o r c h a p t e rf o u r ：g i v i n gs o m ee x a m p l e s k e 】n w o r d s ：r u l e s ，a u t o m a t e d r e a s o n i n g ，f o r , a r d c h a i n ，s e n t e n c e s ， c o n t r a r y 广州大学学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指 导下，独立进行研究工作所取得的成果。除文中已经注明引 用的内容外，本论文不含任何其他个人或集体已经发表或撰 写过的作品成果。对本文的研究做出重要贡献的个人和集体， 均已在文中以明确方式标明。本人完全意识到本声明的法律 后果由本人承担。 学位论文作者签名：棚 日期： 艚石月日 广州大学学位论文版权使用授权书 本人授权广州大学有权保留并向国家有关部门或机构送 交论文的复印件和磁盘，允许论文被查阅和借阅。本人授权 广州大学可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇 编学位论文。( 保密的学位论文在解密后适用本授权书) 学位论文作者签名排 导师签名：季佗幸 e t 期：肼月，日 日期：瑚饵日 l 蟹监 一一 一一 1绪论 1 1 自动推理的历史及发展 用机械的方法解决千变万化的几何问题，是早在十七世纪l e i b n z 就开始幻想的 课题，也曾是历史上一些卓越的科学家的梦想。 2 0 世纪初，德国数学家希尔伯特在几何基础中的一个定理表明，初等几何中 只涉及关联性质的定理可以实现证明的机械化【2 “。 所谓“关联性质”，指的是“某点在直线上”，“某直线过某点”，“两直线平行”等 等这类不涉及线段长度，角度大小以及垂直，相似等的几何性质。 希尔伯特对命题的要求太高，在当时只解决了很小的一类几何定理的机器证明问 题，但却是第一次真正提出了对某类几何命题的机械化检验方法。 1 9 5 0 年，波兰数学家塔斯基发表了一条引人注目的定理( 塔斯基定理) ：“一切初 等几何和初等代数范围的命题，都可以用机械化方法判定” 3 ，2 那。 塔斯基定理的证明是构造性的。也就是说，他确实提出了一套能判定任一个初等 几何或初等代数命题的机械化方法。可是这方法的计算复杂度太大了。即使用快速的 计算机，也不能在合理的时间内，证明稍微难点的几何定理。 1 9 5 9 年，美国华人王浩教授只用9 分钟的机器时间，就在计算机上证明了罗素和 怀特海数学原理一书中的一阶逻辑部分的全部定理3 5 0 多条，引起数学界的轰动， 也宣告了用计算机进行定理证明的可能性，同时也证明完善机械证明的理论及算法是 提高机器证明效率的重要因素。 1 9 6 5 年美国数学家鲁滨逊提出了著名的归结原理，虽过于一般，不能借助它证 明高难的定理，但对后续的研究产生了积极的影响。1 9 7 6 年，美国数学家阿佩尔和 黑肯借助于计算机，成功地证明了“四色猜想”，这是机器证明首次解决传统人脑支 配的手工证明所没有解决的重要难题 3 _ ，“。 1 9 7 7 年，我国著名的数学家吴文俊院士在中国科学杂志上发表了题为“初等几 何判定问题与机械化证明”的论文，提出了一个证明等式型初等几何定理的新的代数 l 绪诠 一 方法。这个方法虽然不能证明几何不等式，但在证明等式型几何定理时效率比以前的 方法高得多。1 9 8 4 年，周威青在他的博士论文中把这个方法叫做吴法1 4 , 5 1 ，并列举了 他基于吴法所编写的程序证明的1 3 0 个非平凡的几何定理。不久，他又在一本专著中 列出了用吴法证明的5 1 2 个几何定理。吴法从此在国际自动推理研究领域广为传播。 希望用计算机生成几何定理可读证明，即易于为人们理解和检验的较简短的证明 的研究，早在6 0 年代已经开始了，在吴法成功之后，这方面的努力并没有停止。在 吴消元法的启发下，1 9 9 2 年提出了以面积关系为工具的消点法l0 1 ，这一机械化的 算法不仅能够对数以百计的困难的几何定理在计算机上飞快地得到证明，而且还能由 计算机自动生成可读证明。几何定理机器证明的研究，由此进入了一个新的阶段。 1 9 9 2 年，中科院张景中院士访问美国进行合作研究期间，将他从前提出的系统 的面积解题方法用于机器证明的研究，在与周成青，离小山的几个月合作研究中，成 功地研究出具有可读性的几何定理自动生成的机器证明软件，在计算机上产生了4 0 0 多条非平凡的几何定理的可读证明。使人们期待了近3 0 年的可读性证明第一次在计 算机上实现。从而在几何定理可读机器证明方面取得突破性进展。目前的几何定理机 器证明的文献中通常把该方法称为消点法或面积法。消点法在几何定理机器证明中开 辟了一个新的纪元。 从1 9 9 7 年以后，张景中院士将其多年的研究成果，应用到我国的中学教育事业 上。领导开发了面向中学数学的智能教育软件，开辟了自动推理应用的新的领域。 1 。2 几何阿题机器求解的几种主要推理方法 1 2 1坐标法 1 9 7 7 年，我国著名数学家吴文俊先生提出了用代数的方法来证明几何定理的新 方法，该方法称为吴法。用吴法可在微机上用几分钟甚至几秒钟证出很不简单的定理。 但吴法适用于证明“等式型”的几何定理。所谓等式型的几何定理：是指可以将几何 问题化为代数问题后，定理的条件和结论都可以化为若干多项等式的形式。 2 ! 缝逾一一 坐标方法的思想是把命题涉及的几何构形中的点坐标化，把命题的条件和结论表 示为坐标的多项式方程组，然后检查条件方程组的解是否满足结论方程组的解。对于 h i l b e r t 交点型定理，条件方程组关于约束变元是线性方程组，因而可以用g u e s s 消元 法求出其解，然后代入结论方程组验证即可。而对于一般的几何命题，条件方程组通 常不是线性的，从而无法从中将约束变元解出。吴法则是不解方程组，而利用伪除法 的方法判定条件方程组的解是否是结论方程组的解。多项式的伪除法可以用符号演算 的方法在计算机上实现。 1 2 2 面积法 以吴法为代表的坐标方法能够告诉人们的只是某类命题的真假。这些方法给出的 证明一般都非常复杂，其中涉及大量的多项式计算或数值计算。这些不像传统的证明 那样，简洁，明了。它告诉人们的是某个命题的真假，但很难读懂其原因。因此， 给出几何命题的让人能读懂的证明过程的问题在多次机器证明的学术会议上被许多 专家学者提出。 其实，希望用计算机自动生成几何定理的可读证明的研究工作早在1 9 6 0 年就已 开始。这方面的著作也发表了很多，但进展不大。直到1 9 9 2 年，仍未找到哪怕是对 一小类几何定理能生成可读证明的有效算法。如何让计算机产生简洁可读的证明过程 成为数学家，计算机科学家的一个具有挑战性的课题。 1 9 9 2 年，中科院张景中院士访问美国进行合作研究期间，基于他以前发展的系 统的面积解题方法f 9 , 1 0 ，提出了几何定理机器证明的新方法，即所谓的面积法或消点 法。 该方法包括一组作图规则，一组几何量和关于这些规则，几何量的一组消点公式。 对于一个给定的几何命题，先按规则作出图形，在作图过程中产生一组点的等式型约 束条件。把命题结论表示为图中几何量的一个等式。证明的过程是利用消点公式，按 与作图( 作点) 时的相反顺序将结论等式中的点一个个逐步消掉。 用面积法不但能在计算机上实现定理的可读证明，而且能不借助于计算机而 蟹熊 用手工实现。因为它产生的证明往往十分简洁。对于给定的一个几何命题，按作图规 则顺序产生各点，然后从结论等式中利用消点公式以相反的顺序消去各点，从而得到 证明。这一工作被一些国际著名的计算机科学家称为“计算机处理几何问题发展路上 的里程碑”。 1 2 3 搜索法 以面积法为代表的几何量法，尽管能给出大类几何定理的通用证明方法，并产 生可读证明。但证明的过程不能够完全合乎人们通常的习惯。因而，我们需要有可读 性更强的证明，希望有更合乎人们思维习惯，更接近普通文献和教科书中人工表达方 式的证明。人在证明几何定理时，通常是依据常用的引理，定理，已知条件，用逻辑 推理规则作各种可能的搜索，去寻找图中更多的性质，将搜索到的信息作为进一步搜 索的基础，直到希望证明的结论被找到。 实际上，这样的想法在机器证明研究最开始就有。早在1 9 6 0 年就有论文发表， 3 0 多年来，关于这方面的研究有不少著作，并写了一些试验性的程序或用于计算机 辅助教学程序。由于遇到搜索空间过大和辅助线的困难，这种方法直到1 9 9 5 年为止， 未能形成能处理成类的几何命题的有效算法。从发表的2 0 多个例子来看，多属于中 学课程的内容，且仅涉及直线形，且未见有达到不动点( 即一切可能的信息) 的报道。 1 9 9 6 年，张景中，高小山，周咸青提出一个基于前推的模式设计的“几何信息 搜索系统”或“几何推理数据库”。利用o l s s 系统编制的c 程序证明了1 6 1 个非平凡 的几何命题，且均在合理的时间内达到不动点，并能证得其它方法不能证明的命题。 用前推法搜索几何信息，其原始思想被称为“大英博物馆”方法，是一种古老的想法。 搜索法的主要困难在于控制几何信息的膨胀。在g i s s 中使用了全角的方法和等价类 的方法来控制几何信息的膨胀“6 。”1 ，取得的很大的成功。 目前，基于前推搜索法的几何定理机器证明软件已进入实用阶段，走进了中学教 学领域。 4 ! 缝监 一一 1 3 自动推理软件的应用 随着计算机辅助教学的发展，广大的教育工作者一直希望，能有更好的教学软件 应用在教学上，特别是用在中学数理化教学上，有不少的科技工作者在致力于这方面 的工作，也取得一定成效。 进入九十年代，教育软件形成了广阔的市场，吸引了众多i t 企业，教研单位加 入到教育软件的行列中，教育软件走上蓬勃发展的大道。到了九十年代中期，中国的 教育软件百家争鸣，迎来发展黄金期。九十年代末期，人们对教育软件提出更高的要 求。那种题库式的软件模式已不能满足人们的要求，也不符合当前的素质教育需要。 人们希望计算机能和人进行交互解题，能在解题过程中给人启发。 随着教育软件的发展，现在教育软件已经进入了一个新的时代。新一代的教育软 件应具备如下特点【1 8 】： 1 ) 界面美观，生动有趣。 2 ) 内容丰富，实用性强。 3 ) 操作方便，简单宜学。 4 ) 课件制作，动态作图。 5 ) 智能解题，自动推理。 其中，新一代教育软件的主要特点就是能够进行智能解题，增强了人与计算机之 间的交互性。 现在，有关教育方面的商品软件琳琅满目，从小学教育到大学教育，应有尽有， 但这些软件大都不具备自动推理的能力。确实，要让计算机自动给出合乎人们习惯的， 简短的推理过程，不是一件容易的事情。 g i s s ，g e r o m e t r ye x p l o r e r 是自动推理在中学教育中比较成功的应用。该类软 件能在一个合理的时间内，对大多数中学的平面几何命题给出符合人们阅读习惯的 传统证明过程。该软件提供的人机交互功能，可以通过使用者与计算机之间对话自动 生成解题过程，有效地启发学生的思维和指导学生解题的方法。因而，它一出现就受 到广大中小学教师，学生的欢迎。随后，张景中院士领导的小组相继成功开发了立体 ! 绮途 一 几何，解析几何等智能教育软件。 证明与推理，是智能的高级表现形式，智能教育软件的出现，开辟了几何定理机 器证明的新的应用领域，同时也改变了教育软件的面貌。我们有理由相信，在不久的 将来，智能教育软件必将成为教育软件的主流方向，成为广大教师，学生的得力助手。 1 4本文的工作 从手工证明到机器证明，是数学思想方法的重大飞跃。而计算机能产生传统的可 读证明过程，又是机器证明领域的重大突破。将几何定理可读证明应用于教学，特别 是中学教学，是具有远见卓识的想法。智能教育软件的出现，将自动推理融入教育软 件中，改变了传统的教育软件模式，适应了中小学教育从应试教育向素质教育的转变 的要求。将课本上的知识教会计算机，计算机运用这些知识，对用户给出的命题进行 分析，推理，然后输出结果。因此，要让计算机能够证明几何题目，首先要教会计算 机证题的方法。实际上是人类把数学证明的一些方法教给计算机，计算机通过这个方 法来证明。所以教会计算机方法是主要的。 数学证明方法可分为直接证法和间接证法，对于不同的题目适合用不同的方法。 1 直接证法：从原命题所给的条件出发，根据已有的公理、定义、法则、公式， 通过一系列的推理，一直推到所要证明的命题的结论。 2 间接证法：间接证法是通过以下途径的数学证明方法： ( 1 ) 通过论证原命题的反论题( 即与原论题相矛盾的命题) 为假，从而论证了原命 题为真。 ( 2 ) 通过论证与原命题等价的命题为真，从而达到论证原命题为真。 计算机技术的发展及可读证明的出现，使自动推理在中学教育中得到比较成功的 应用，其中也相应地出现了许多推理方法，如坐标法，几何不变量法，搜索法等，比 较常用的是前推搜索法，因为它能生成较为传统的可读证明过程【5 1 。 使用前推搜索法进行自动推理，除了要教会计算机如何推理外，最基本的是要让 计算机知道推理的规则，这些规则就是我们通常的公理，定理，定义，引理等等。计 ! 缝迨 一 算机根据己知条件，运用规则进行推理，直至推出所证结论或推理达到不动点【5 】。从 数学证明方法上而言是属于直接证法。这些规则中的条件与结论都是以肯定的形式存 在的，这种方法要求命题的结论必须是肯定。是由真前提推出真结论。但对于一些否 定性命题，唯一性命题，或结论中以“至多”，“至少”形式出现的命题，由于使用 的规则很少有推出否定性，或唯一牲的结论，对于这类问题如果采用上述方法直接从 已知条件出发，利用规则进行推理，就很难推出结论。这对需要采用数学证明中的 间接证法来证明，数学中常用的间接证法有反证法。 反证法是几何证明方法中很重要的一种方法，反证法的题目在平面几何中也占有 很重要的一部分。园此，有必要将反证法引入自动接理中，使其更加完善。同时一些 专家系统和知识工程的出现【2 5 】，也使人们认识到，仅仅研究那些从真前提推出真结论 的逻辑推理方法是不够的。 尽管几何定理祝器证明的研究在七十年代已经取得突破，可读证明的实现也近十 年了，自动推理的软件也出现了很多，但很少有在自动推理中实现间接证法的。只 有在z + z 智能教育软件中的平面几何中有同一法，而其他的一些教学软件( 如 翰林汇，科利华，嘉科平面几何) ”，擂，1 9 1 中仍未出现过。这使自动推理软件在解决 需要间接证明的题目时存在一些不足。本文的工作就是向这个方向努力的一个尝试， 将间接证法中的反证法与自动推理中使用较多的前推搜索法相结合，使自动推理在证 题方面更加完善。 采用前推搜索法进行几何定理机器证明，控制推理信息库的膨胀非常重要。在搜 索的表示方法中，角度和比例线段的处理是引起膨胀的两个主要因素。在本文主要采 取了以下措施控制信息的膨胀： 1 合理选择谓词。选择的谓词要尽可能反映平面几何关系，但同时要考虑其带 来的复杂性。 2 数据的合理组织。如归一化，退化处理。 3 采用与传统角度记法不同的表示方法。我们知道，传统可读证明是以传统角 的形式表示的。我们采用另外的简化的表示方法，压缩了信息。 4 对于线段相等，比例线段等，采用合理的存放方式。 5 对于信息采用压缩的形式存放。 ! 缝迨 一 总之，有效控制信息的膨胀会大大提高推理速度。 作为教学目的的智能教育软件系统，不仅要提供自动推理的过程，而且还要给出 用户对命题输入的功能。使用户能够简单操作。 本系统主要有以下功能： 1方便，快捷的绘图工具。能够完成几何图形的简单输入。 2 图形的智能性，动态性。提供一些图形工具，在作图的同时生成图形所蕴含 的条件，图形的移动过程中，各种几何关系不变。 3 提供不同的输出。将推理的结果以两种形式输出，便于分析和阅读。 4 方便的命题输入系统。可以在作图时将作图过程产生的信息自动生成已知信 息，也可以采用本系统提供的工具进行输入。 5 快速的推理系统。通过对信息的压缩，程序结构的优化，搜索算法的改进， 加快推理速度。 6 实现反证法证题。 2 垣堡褪渣主篮丕塞毽 2原理概述与技术实现 2 1 原理概述 反证法是一种间接证法，反证法是指“证明某个命题时，先假设它的结论的否定 成立，然后从这个假设出发，根据命题的条件和已知的定理，公理等经过推理，得出 与已知事实( 条件、公理、定义、定理、法则、公式等) 相矛盾的结果这样，就证 明了结论的否定不成立，从而间接地肯定了原命题的结论成立。 用反证法证题一般分为三个步骤： 1 假设命题的结论不成立。 2 从这个结论出发，经过推理论证，得出矛盾。 3 由矛盾判定假设不正确，从而肯定命题的结论正确。 即：提出假设推出矛盾一肯定结论。 一般宜用反证法的命题有： 1 对于结论是否定形式的命题，宜用反证法。 2 对于证明结论是“唯一”或“必然”的命题，宜用反证法。 3 对于证明结论是“至少”，或“至多”的命题，宜用反证法。 4 有些命题的证明，可利用的公理、定理较少或者难以与已知条件相沟通，宜用 反证法。 由于命题结论的不同情形，对结论的否定也会出现不同的情形。根据命题结论的 否定情形不同，反证法又可分为归谬法和穷举法，当对原命题结论否定情形只有一种 时为归谬法，当对原命题结论否定情形不止一种( 但是有限种) 时为穷举法。 利用反证法首先要对命题的结论进行否定，对于归谬法，结论的否定情形只有一 种，我们只需要在系统中设置一些对立的表述形式，在对结论进行否定时，只需要找 到与它对立的信息即可。本文已经做了这方面的处理。但对于穷举法，结论的否定情 形不止一种，可能会有两种或多种。 9 2 厘堡掇述皇挂丕塞理 在多种情形中，当结论是至多型时。如需要证明z a b c 与z a c b 中至多有一个 为9 0 。，那么对该结论否定后就应是：假设l a b c = 9 0 。与z a c b = 9 0 4 。对于这 一类的命题，在对结论进行反设时，只需要将反设的结果全部存放在对应的信息表中 即可。 在多种情形中，结论不是至多型的，反设后的情形不是同一类型。如：需要证明 z a b c = 9 0 。那么在反设后就是：假设z a b c 9 0 。，l a b c 么g h k 角度和的不等关系 d e f 一1g h k ) ( 可输入多个角) c s u m s e gc s u m s e g ( 1a b1 c d a b + c d e f 线段和的不等关系 一1 g h )( 可输入多个线 段) n o t e q u a l s e gn o t e q u a l s e g ( a ba b c d两线段长度不等 c o ) n o t e q u a l a n gn o t e q u a l a n g ( a b c 么a b e d e f 两角度不等 d e f ) 1 4 2 愿堡燕述兰撞鲞塞毽 续表2 3 1 n o t p a r a l l e l n o t p a r a l l e l ( a bc d ) a b 与c d 不平行两线段不平行 a t m o s t z a x i a n g ( i n f o l ， i n f o ；i n f o 。中至多有至多( 可输入多个 i n f 0 2 ，i n f o n ，m )m 个成立信息) c o n t r a r y c o n t r a r y ( i n f o i ，i n f 0 2 )i n f o 。与i n f 0 2 矛盾两信息矛盾 2 3 2 语句结构及语句的标准化 ( 1 )语句结构 在推理的过程中，用到的有推理规则，已知条件和新的结论。对于推理过程产生 的语句，存放在几何信息库中。通常的作法是，对于每一个语旬( 不论是新推出的还 是初始条件) ，都构造一个对象，然后在计算机内存中以链表的形式存放。 一条语句总包含若干个点，对于有些语句，还会有参数，有些语句存放的不是点， 而是几个对象。在我们的系统中，语句主要有三种类型： 不含参数：如三角形相似，平行四边形等。 含有一个参数：如已知的角度，已知的线段长度等。 存放两个对象：如两线段相等，两角度相等，比例线段等。 在这三种类型中有非常多的共性。在定义数据结构描述语句时，我们将他们归结 为同一个类来描述。对于存放点的语句，将点放在个表m _ n p o i n t s 中：对于含一个 参数的语句我们我们增加一个变量mn v a l u e ； 对于存放两个对象的语句，我们增 加一个数组1 t l n l n f o 来存放。根据这个类的实例( 即对象) ，各个语句组根据参数 的不同缺省，就能构造出不同的几何信息。 下面是语句的结构： c l a s sa f x e x t c l a s s c l n f o ：p u b l i cc o b j e c t i n f o t y p em _ n t y p e ：语句的类型( 谓词) 2 厘堡揠姿皇燕丕塞翌 c l n f o a r r a ym _ n l n f o ：存放对象 c u i n t a r r a ymn p o i n t s ：存放点 b o o lmb e q u a l ：是否有等号 b o o lmb v a l u e ：是否有值 c o e f f t y p em _ n v a l u e ： 语句的值 i n f o t y p em _ e r e a s o n 5 ： 理由的谓词 i n tmn r e a s o n n o 5 ：理由谓词对应的号码 i n tmn s d e c i a l r e a s o n n o 1 0 ： i n tmn r u l e ：规则 b o o lmb u s e ：是否可用 i n tm _ n l n d e x ：在信息表中的位置 ( 2 )语句的标准化 对于一条语句，我们有许多种表达方式。如：对于线段a b 和c d 平行，就可以写 成p a r a l l e l ( a b ，c d ) ，p a r a l l e ( a b ，d c ) ，p a r a l l e l ( b a ，c d ) ，p a r a l l e l ( b a ，d c ) ， p a r a l l e l ( c d ，a b ) ，p a r a l l e ( c d ，b a ) ，p a r a l l e l ( d c ，a b ) ，p a r a l l e l ( d c ，b a ) 而这 8 种表达式本质上表现的是同一几何事实。 对于四点共圆有2 4 种记法，而四条线段成比例则有2 5 6 种写法。 如果将同一几何事实的不同记法全部作为推理信息记录，势必造成推理信息库的 急剧膨胀。因此，我们要将语句标准化，其目的就是使得对于几何命题中出现的每一 几何事实，都能用同一条语句记录。 首先，我们定义几种记号： p 。 = p 。表示p ，点的名字大于等于p 。的名字。 p 。 = p ：表示p 点的名字小于等于p 。的名字。 2 厘堡援蓬兰蕴丕基翌 p 。= m i n ( p ：，p ：，p 。)表示p 。名字在p 。，p 。，p 。中最小。 p 。= m a x ( p ，p 2 j ”，p 。) 表示p 名字在p 。，p 2 一，p 。中最大。 p ，p 。，p 。 = q l ，q 。，q 。表示p ，p ”，p 。各点名字组成的字符串小于等于 q 。，q ：，q o 各点名字组成的字符串。 下面是各类语句的标准化结果。 1 ) m i d p o i n t ( p ，p 。p 。) p 。 p ，p 。，p ：，p ，是命题中的三个点，p 。是中点。 2 ) p a r a l l e l ( p 。p ：p 。p ) p 。= m i n ( p 。，p ：，p 。，p 。) ，p 。与p 3 在线段p 2 p 。的 同侧。p p 。是第一条线段，p 3 p 。是第二条线段。 3 ) v e r t i c a l ( p ip ：p 。p 4 ) ，p = m i n ( p ，p 2 ，p 。，p 。) ，p , p 。是第一条线段，p 。r 是第二条线段。 4 ) s e g m e n t ( p p 2 ) p ，p 。是线段的两个端点，p ，( p 。 5 ) s e g m e n t v a l u e ( p 。p ：l ) p ，p 2 是命题中的两个点，p p 。 6 ) e q u a l o f s e g m e n t ( p lp 2p 。p ) p j = m i n ( p 。，p ：，p np ) ，p 。 p ，p , p 2 是 第一条线段，k p 。是第二条线段。 7 ) a n g l e ( p p ：p 。) p 。是角的顶点，p 。，p 。，p 3 饶逆时针方向旋转。 8 ) a n g l e v a l u e ( p ，p ：p 。a ) p 。是角的顶点，p 。，p z ，p a 饶逆时针方向旋转。 9 ) e q u a l o f a n g l e ( p p ：p 。rp sp 6 ) p 。，p 6 是角的顶点，p 。 p 5 ，p ，p ：，p 。 饶逆时针方向旋转，p ；，p ；，p 8 饶逆时针方向旋转。p , p 。p 。是第一个角，p 4 p ；p 。 是第二个角。 1 0 ) t r i a n g l e 一9 0 ( p ，p ：p 3 ) p 2 是直角顶点，p t p 3 。 1 1 ) i s ot r i a n g l e ( p 。p 。p 。) p ：是顶点，p ： p 3 。 1 2 ) c o n t r i a n g l e ( p 。p 2p 3 ) p ； p z p a ，p 。，p 2 ，p 3 是三角形的三个顶点。 1 3 ) e q u i l t r i a n g l e ( p 。p ：p 。r p sp e ) p , p 。p 。是第一个三角形，p 。p 5 p 6 是第二 个三角形，p 。= m i n ( p ，p 。，p 3 ，p 。，p 。，p 6 ) ，p 。 p ， p 。，p , p ：p 。 p 4 p 。r ，r k p 6 的位置变换要随p 。p ? p 3 的变化。 1 4 ) p a r a l l e l o g r a m ( p 。p zp ，一) 。p t = m i n ( p ，p p a ，p 。) ，p , p ：p 。p 。依逆时针方向 旋转。 1 5 ) r e c t a n g l e ( p ，p 2p 。r ) 。p ，= m i n ( p 。，r ，p 。， ) ，p ，p 2 p 。r 依逆时针方向旋转。 1 7 2 愿垄援适量燕丕塞丑 1 6 ) s q h g r e ( p p 2p ，p 。) 。p 。= m i n ( p 。，p ：，p 3 ，p 。) p , p z p 。r 依逆时针方向旋转。 1 7 ) r h o m b u s ( p ，p 。p 。p 。) p = m i n ( p 。，p 。，p 3 p 。) p , p 。p 。p 。依逆时针方向旋 转。 1 8 ) e c h e l o n ( p ，p 2p 。p 。) p ，p 2 p 3 p 。，p , p 。是上底，p ， p 2 ，p ，与p 3 在线段 p 2 p 。的同侧。 1 9 ) i s 0 5 r a p e ( p p ：p 。p 。) p , p 。p 。p 4 ，p i p z 是上底，p p ：，p 与p 。在线 段p 2 p 。的同侧。 2 0 ) h u b u a ( p ，p ：p 。p 。p ；p 6 ) p , p 。p 。是第一个角，p 4 p 。p 。是第二个角，p ：，p 。 是角的顶点。p 。 p 。 2 1 ) h u y u a ( p p 2p 。p 。p 5p 6 ) p , p 。r 是第一个角，p 。p 。p 。是第二个角，p ! ，p ；是 角的顶点。p ： p 。 2 2 ) s u m a a ( a ，p 、p 。p ，a ：p 。p 。p 。) p 。p 。p 。是第一个角，a 是第一个角的系 数，r p ；p 。是第二个角，a ：是第二个角的系数。p 。，r 是角的顶点。 2 3 ) s u m s e g ( a ，p ，p 。a zp 。p 4 ) p , p 。是第一条线段，a 是第一条线段的系数， p 。p 。是第二条线段，a 2 是第二条线段的系数，p ， p 。，p 。 p 。 2 4 ) h a n g l e l i n e ( p 。p zp sp t ) pl p ：p 。是角，p ：是角的顶点，p 。是角平分线上的 一点。 2 5 ) r a t i o o f s e g m e n t ( p 。p 。p 。p ；p sp 6p ，心) p , p 。是第一条线段，p ，r 是第 二条线段，p ；p 6 是第三条线段p t p 。是第四条线段。其中p ，= m i n ( p ，p 。，p 。，只，p 。p 。，p ，p 。) 2 6 ) r e s e m _ t r i a n g l e ( p ，p 。p 3p 。p sp 6 ) p , p 2 p s 是第一个三角形，p 4 p 。p 。是第二 个三角形p 。= m i n ( p 。，p 。，p 3 ，p 4 ，p 。，p 。) ，p ， p ： p 。r p ；p 6 的顺序随p , p ：p 。的顺序而 变。 2 7 ) c s u m a a ( a 。p ，p ：p aa 。p p 。p 6 ) p i p ：p a 是第一个角，a ，是第一个角的 系数，p 4 p 。p 。是第二个角，赴是第二个角的系数。p 2 ，p 5 是角的顶点。 2 8 ) c s u m s e g ( a 。p 。p 。a zp ap t ) p 。p 2 是第一条线段，a ：是第一条线段的系数， p 3 p 。是第二条线段，a 2 是第二条线段的系数，p 。 p 。，p ， p 4 2 9 ) n o t e q u a l s e g ( p - p zp 。r ) p , p z 是第一条线段，p 。只是第二条线段。 p ，= m i n ( p l ，p 2 ，p 3 ，p d ) 1 8 2 匾堡艇蓬皇越丕塞强 一一 3 0 ) n o t e q u a l a n g l e ( p ，p 。p 。p 。p 5p 6 ) p j p 2 p 。是第一个角，p , p 6 p s 是第二个角a p 。 = p 5 3 1 ) n o r ? a r m l e l ( p p ：p 。r ) p , p 2 是第一条线段，p 。只是第二条线段，p = m i n ( p 。p 。p 。p ，) ，p 2 p 。在p , p a 的同侧。 2 3 3退化情形处理 在欧几里德几何中的几何关系中，通常都假设了某种非退化性。如三角形就假定 了三个顶点不在一条直线上：平行的两条直线不重合等等。这些命题都无需说明，几 何图形非常直观地给出了这些信息。 退化的信息，对推理的影响也是两方面的： ( 1 ) 推出一些错误的结论。如对于三角形a b c ，我们说如果z a b c = l a c b ， 则有a b = a c 对于非退化的情形是对的，但如果该三角形的三个点在一条直线上如 ( 图3 3 1 ) ，l a b c = z a c b = 0 。，由于a 可以在b c 之间的任意位置，因此a b = a c 是错误的。 ? 娶 c ( 图3 3 1 ) ( 2 ) 大量没有意义的信息存在，导致推理信息急剧膨胀，大大降低推理速度。如 c 是a b 的中点，由于c a ：c b ，c a b 是等腰三角形，而由c a b 是等硬三角形 得到么c a b = l c b a 为了避免推理时的退化情形，在向信息表中添加一条新的信息时首先对这条信息 进行是否是退化信息的检查。如果是退化信息，就不向表中添加。这样在推理时，保 证了从表中提取的信息都不是退化的。减少了许多无效的匹配。 首先是对一些基本信息退化的定义： 定义3 3 1 ：如果一条线段的两端点重台，称这条线段是退化的。如线段从 定义3 3 2 ：如果一个三角形有两个或三个顶点重合，或三个点在一条直线 上，则认为该三角形是退化的。如a b b