动态几何软件(Dynamic Geometry Software)与普通的作图软件有着本质上的不同。它绘制的几何图形不但精确,而且还具有动态性,这使其非常适合于几何教学的实际需要。动态几何软件已经成为了几何教学的强有力工具,对几何教学的现代化改革产生了重大而又深远的影响。然而,教育的实际应用也逐渐暴露了动态几何软件的很多缺陷。其主要缺陷是动态几何不具有智能性。缺少智能性是制约动态几何软件有效应用的瓶颈。这里,智能性是指动态几何软件能象“几何专家”一样帮助用户解题。本文把这种具有专家级解题能力的动态几何软件称为智能几何软件(IntelligentGeometry Software)。智能几何软件不但能动态作图而且还能自动解题。这使其能更好地帮助学生学习几何证明。应用几何定理机器证明的研究成果,可以研制出高智能的几何教育软件。这只需在动态几何软件中嵌入一个定理证明器,就可以简单地实现具有专家级解题能力的智能几何软件。目前,研制成功的智能几何软件已经走进了中学几何教学的课堂,比如《几何专家》,《超级画板》,《体验数学—Math Xp》等等。定理证明器是智能几何软件的推理引擎的核心程序。大多数智能几何软件都使用基于前推法(forward chaining method)的定理证明器作为推理引擎。这是因为前推法能给出易于学生理解、易于检验的传统证明。但是,前推法还存在着有很多不足,比如推理效率比较低,解题能力有很大的局限性。为了进一步提高前推法的推理效率和增强前推法的解题能力,以便使智能几何软件能更好地满足几何教学的实际需要,本文针对前推法提出以下3种改进技术:1.将Rete模式匹配算法整合到前推法的推理引擎中,构造了一种具有高匹配效率的前推法推理引擎。本文把这种推理引擎为几何自动推理网。几何自动推理网把规则集转换成数据流网,用数据流网来动态地保存推理规则和几何信息的匹配状态。通过消除推理过程中冗余匹配来提高推理效率。2.为了提高前推法对几何等价信息的推理效率,提出了一种高效的等价类推理方法。该方法包括两种技术:(1)使用等价类合并推理规则替换等价谓词的传递推理规则。(2)使用等价类代换推理规则替换等词的代换推理规