学位论文 > 优秀研究生学位论文题录展示

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

作　者: 江建国
导　师: 张景中
学　校: 中国科学院研究生院（成都计算机应用研究所）
专　业: 计算机软件与理论
关键词: 几何定理机器证明定理证明器动态几何软件智能几何软件搜索法可读证明前推法
分类号: TP319
类　型: 博士论文
年　份: 2006年
下　载: 275次
引　用: 2次
阅　读: 论文下载

内容摘要

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

全文目录

摘要  3-5
Abstract  5-8
目录  8-18
第一章引言  18-36
  1.1 研究背景与研究主题.  18-24
    1.1.1 动态几何软件  18-20
    1.1.2 智能几何软件  20-24
  1.2 研究现状  24-31
    1.2.1 国外研究状况  24-28
    1.2.2 国内研究现状  28-31
  1.3 研究内容与研究意义  31-34
  1.4 本文结构概览  34-36
第二章几何定理机器证明  36-84
  2.1 几何定理机器证明概述  36-43
    2.1.1 初期阶段  36-39
    2.1.2 中期阶段  39-41
    2.1.3 近期阶段  41-43
  2.2 几何  43-55
    2.2.1 欧几里得几何  43-45
    2.2.2 希尔伯特几何  45-51
    2.2.3 塔斯基几何  51-54
    2.2.4 中学平面几何  54-55
  2.3 几何知识表示  55-62
    2.3.1 一阶逻辑法  55-58
    2.3.2 坐标法  58-61
    2.3.3 自由坐标法  61-62
  2.4 几何定理机器证明法  62-81
    2.4.1 代数法  62-75
    2.4.2 人工智能法  75-81
  2.5 几何定理证明器  81-84
第三章定理证明器iGeo  84-98
  3.1 基于规则的专家系统  84-87
    3.1.1 系统结构  84-85
    3.1.2 推理方向  85-87
  3.2 iGeo的系统结构  87-88
  3.3 iGeo 的知识表示  88-96
    3.3.1 几何图形  88-90
    3.3.2 几何对象  90-92
    3.3.3 几何谓词  92-96
  3.4 iGeo 的规则集  96-98
第四章几何自动推理网  98-116
  4.1 引言  98
  4.2 Rete算法  98-105
    4.2.1 临时冗余与结构相似  98-101
    4.2.2 模式网与结合网  101-105
  4.3 几何自动推理网  105-108
    4.3.1 几何自动推理网的结构  105-106
    4.3.2 几何自动推理网的算法  106-108
  4.4 实现与实验  108-113
  4.5 小结  113-116
第五章等价类推理技术  116-126
  5.1 引言  116-117
  5.2 几何等价谓词和几何等词  117-119
    5.2.1 几何等价谓词  117-118
    5.2.2 几何等词  118-119
  5.3 传递和代换推理规则  119-120
    5.3.1 传递推理规则  119-120
    5.3.2 代换推理规则  120
  5.4 推理效率分析  120-122
    5.4.1 传递推理效率分析  120-121
    5.4.2 代换推理效率分析  121-122
  5.5 等价类推理  122-124
    5.5.1 等价类合并推理规则  122-123
    5.5.2 等价类代换推理规则  123-124
  5.6 实现与实验  124-125
  5.7 小结  125-126
第六章几何量多项式等式型定理的可读证明  126-138
  6.1 引言  126-127
  6.2 几何量多项式等式  127-129
    6.2.1 多项式等式  128
    6.2.2 多项式的标准型  128-129
  6.3 多项式的恒等变换  129-132
    6.3.1 标准项代换  129-130
    6.3.2 算例  130-132
  6.4 几何量多项式等式型定理的推理算法  132-134
  6.5 实现与实验  134-137
  6.6 小结  137-138
第七章定理证明器iGeo 的Lisp实现  138-152
  7.1 证明器iGeo 的主程序  138-139
  7.2 生成几何对象库  139-140
  7.3 AGRN网前向搜索  140-143
  7.4 等价类推理的实现  143-144
  7.5 几何量多项式等式型定理推理的实现  144-152
第八章结语与进一步工作  152-156
  8.1 结语  152-153
  8.2 进一步工作  153-156
附录A iGeo 的推理规则库  156-162
附录B 几何命题测试库1  162-170
附录C 几何命题测试库2  170-199
发表文章目录  199-200
简历  200-201
致谢  201-202

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

内容摘要

全文目录

相似论文