iGeo：智能几何软件的定理证明器

论文摘要

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

论文目录

• 摘要
• Abstract
• 目录
• 第一章 引言
• 1.1 研究背景与研究主题.
• 1.1.1 动态几何软件
• 1.1.2 智能几何软件
• 1.2 研究现状
• 1.2.1 国外研究状况
• 1.2.2 国内研究现状
• 1.3 研究内容与研究意义
• 1.4 本文结构概览
• 第二章 几何定理机器证明
• 2.1 几何定理机器证明概述
• 2.1.1 初期阶段
• 2.1.2 中期阶段
• 2.1.3 近期阶段
• 2.2 几何
• 2.2.1 欧几里得几何
• 2.2.2 希尔伯特几何
• 2.2.3 塔斯基几何
• 2.2.4 中学平面几何
• 2.3 几何知识表示
• 2.3.1 一阶逻辑法
• 2.3.2 坐标法
• 2.3.3 自由坐标法
• 2.4 几何定理机器证明法
• 2.4.1 代数法
• 2.4.2 人工智能法
• 2.5 几何定理证明器
• 第三章 定理证明器iGeo
• 3.1 基于规则的专家系统
• 3.1.1 系统结构
• 3.1.2 推理方向
• 3.2 iGeo的系统结构
• 3.3 iGeo 的知识表示
• 3.3.1 几何图形
• 3.3.2 几何对象
• 3.3.3 几何谓词
• 3.4 iGeo 的规则集
• 第四章 几何自动推理网
• 4.1 引言
• 4.2 Rete算法
• 4.2.1 临时冗余与结构相似
• 4.2.2 模式网与结合网
• 4.3 几何自动推理网
• 4.3.1 几何自动推理网的结构
• 4.3.2 几何自动推理网的算法
• 4.4 实现与实验
• 4.5 小结
• 第五章 等价类推理技术
• 5.1 引言
• 5.2 几何等价谓词和几何等词
• 5.2.1 几何等价谓词
• 5.2.2 几何等词
• 5.3 传递和代换推理规则
• 5.3.1 传递推理规则
• 5.3.2 代换推理规则
• 5.4 推理效率分析
• 5.4.1 传递推理效率分析
• 5.4.2 代换推理效率分析
• 5.5 等价类推理
• 5.5.1 等价类合并推理规则
• 5.5.2 等价类代换推理规则
• 5.6 实现与实验
• 5.7 小结
• 第六章 几何量多项式等式型定理的可读证明
• 6.1 引言
• 6.2 几何量多项式等式
• 6.2.1 多项式等式
• 6.2.2 多项式的标准型
• 6.3 多项式的恒等变换
• 6.3.1 标准项代换
• 6.3.2 算例
• 6.4 几何量多项式等式型定理的推理算法
• 6.5 实现与实验
• 6.6 小结
• 第七章 定理证明器iGeo 的Lisp实现
• 7.1 证明器iGeo 的主程序
• 7.2 生成几何对象库
• 7.3 AGRN网前向搜索
• 7.4 等价类推理的实现
• 7.5 几何量多项式等式型定理推理的实现
• 第八章 结语与进一步工作
• 8.1 结语
• 8.2 进一步工作
• 附录A iGeo 的推理规则库
• 附录B 几何命题测试库1
• 附录C 几何命题测试库2
• 发表文章目录
• 简历
• 致谢