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

平面几何的动态可视证明研究

作　者: 叶征
导　师: 童若锋；周咸青
学　校: 浙江大学
专　业: 计算机应用技术
关键词: 动态几何定理证明几何专家可读证明动态可视证明全角法演绎数据库法 JGEX
分类号: TP391.41
类　型: 博士论文
年　份: 2010年
下　载: 78次
引　用: 0次
阅　读: 论文下载

内容摘要

当我们阅读几何书本上的证明的时候,通常需要花费相当的时间和精力来辨识证明文本中的几何元素和几何图形的对应关系。当几何图形或者证明变得复杂的时候,这个问题就会变得很严重。因此,如何在计算机中重新组织和表示几何证明使得它们更容易阅读和理解将是一件十分有意义的事情,这也是证明可视化研究的主要课题之一。本文对平面几何证明可视化方面目前存在的问题进行了深入的研究,其中最主要的是动态几何技术,可读证明的产生、组织以及显示技术等。本文的主要研究目标是为平面几何研究和设计一套能够高效地输入、产生以及表示证明的技术,以帮助用户更好地理解证明。具体的研究内容可以分为以下三个方面：1.研究高效率的方法处理几何图形中的约束关系。几何图形在几何定理的证明过程中起着非常重要的作用。给定一个几何定理,画出其图形并对该图形进行变换的过程可以看做是一个约束求解的过程。传统的约束求解方法没有对约束进行统一的处理,因此在求解效率,稳定性等方面都存在不小的问题。本文研究了如何开发高效的算法对几何图形的约束关系进行求解,希望通过利用平面几何定理的一些特殊性质,能够借助强大的代数方法来求解几何图形中的约束关系。2.研究了专门用于几何定理证明可视化的技术以及输入工具。证明文本和几何图形的对应关系是证明可视化技术的关键。但是对于传统的可读证明来说,这两者是分开的,需要读者在阅读的过程中去比较、识别它们之间的关系。对此,本文研究了平面几何证明的语法结构,希望能够给出几何证明的一般性的结构和组织方式,并且针对这种格式化的证明提出一种可视化方法,使得我们能够把证明文本和证明图形对应起来。另外,本文研究了可视证明的不同产生方法：一方面,考虑提供手动的交互式证明输入工具,让用户使用图形化的工具建立证明。另一方面,考虑提供自动化的方法,充分利用当前几何定理机器证明领域的研究成果,使得用户只需要输入定理文本形式的前提条件就能够自动地产生几何图形以及可视证明。3.研究了动态可视证明的自动产生方法以及证明的层次型组织结构。对于一个复杂的几何定理,当它的证明包含了很多步骤时,如果能够合理组织证明结构,使得证明能够保持在合理的长度之内,对证明的理解显然非常有帮助。对此,本文研究了可读证明的自动产生以及组织方法,希望能够把证明主要的步骤列出来的同时,把次要的步骤隐藏起来,使得用户在阅读时可以抓住证明的重点。本文对以上问题进行了深入研究,并且获得了一系列研究成果。下面是本文的主要贡献和创新点：1.提出了基于构造型几何命题的几何约束求解方法,利用代数方程高效地表示和处理几何图形的约束关系。对于构造型几何命题,根据几何命题中点引进的顺序依次给点的坐标参数赋值,然后把图形中的约束条件转化成代数方程组,该方程组可以很容易地三角化。根据三角化以后的结果,我们可以高效地对图形中的约束进行求解。相比较传统的几何约束处理方法,该方法具有许多优点,例如求解稳定,可以计算出图形的多种可能情况,并且可以对几何图形的一些隐含的性质进行推理和证明等。2.提出了新的基于几何图形的证明表示方法-动态可视证明,提出了几何定理证明的一般语法结构,并且基于这种结构开发了动态可视证明的手动输入方法。动态可视证明最主要的特征是证明的文本和图形的紧密结合。在手动输入方法中,证明的语法结构经过了严格的定义,并且根据这种格式化的证明,采用以鼠标操作为主的输入方式,使得用户可以在事先知道具体证明的情况下很容易地输入动态可视证明。3.提出了基于无序几何模型的动态可视证明自动产生方法：基于全角法的产生方法和基于演绎数据库法的产生方法。这两种方法都是基于无序几何的,非常适合算法实现并且生成动态可视效果。而且,在全角法中,通过结合前推法和后推法,我们提出了证明的层次型组织方法。这种方法使得用户可以把注意力集中在主要的步骤上,而当用户对某些步骤的进一步证明感兴趣时,又可以展开这些步骤,查看它们的详细证明。在演绎数据法中,我们产生一个包含该几何定理的许多信息的数据库,且成功地实现了数据库的可视化。4.基于前面研究成果,我们构造了一款几何定理证明器:Java Geometry Expert (JGEX)。JGEX是一款集成了几何作图、证明以及证明的动态显示为一体的几何软件,它最重要的特性就是实现了我们上面所提到的动态可视证明技术,并且它还提供了手动和自动两种方法产生动态可视证明。利用这些技术,我们已经成功地产生了两百多个动态可视证明的例子。这些技术和例子不仅可以被用于中学几何教学,也可以成为人们学习和研究平面几何证明的有力工具。

全文目录

摘要  3-6
Abstract  6-16
第1章绪论  16-29
  1.1 研究背景和研究意义  16-17
  1.2 研究历史和研究现状  17-26
    1.2.1 平面几何机器证明的发展历史  17-21
    1.2.2 平面几何证明的可视化以及相关工作  21-26
  1.3 本文的研究内容  26-27
  1.4 本文的结构预览  27-29
第2章基于构造型几何命题的几何约束求解方法  29-49
  2.1 基于构造型几何命题的约束求解方法的设计思想  29-30
  2.2 吴方法简介  30-33
  2.3 几何命题的两种输入形式  33-38
    2.3.1 构造形式  33-35
    2.3.2 谓词形式  35-37
    2.3.3 两种输入形式之间的转化算法  37-38
  2.4 基于构造型几何命题的约束求解方法的算法描述  38-41
  2.5 算法的实验结果和分析  41-48
    2.5.1 约束求解的过程稳定  42-44
    2.5.2 可以构造出几何图形的多种可能情况(n≤4)  44-45
    2.5.3 重合点的自动发现和去除  45-47
    2.5.4 非退化条件的自动生成  47-48
  2.6 本章小结  48-49
第3章基于几何图形的动态可视证明技术  49-67
  3.1 可视证明的研究现状  49-50
  3.2 动态可视证明的设计思想以及基本特性  50-53
    3.2.1 动态可视证明的设计思想  50-52
    3.2.2 动态可视证明的基本特性  52-53
  3.3 动态可视证明的手动输入方法  53-66
    3.3.1 方法的基本描述  53-55
    3.3.2 模式一:只有动态图形  55-57
    3.3.3 模式二:自由文本与动态图形结合  57-61
    3.3.4 模式三:预定义的证明文本和动态图形结合  61-65
    3.3.5 实验结果和分析  65-66
  3.4 本章小结  66-67
第4章基于无序几何的动态可视证明自动产生方法  67-99
  4.1 无序几何的理论分析  67-77
    4.1.1 代数证明、无序几何以及有序几何  68-69
    4.1.2 有序几何与传统证明  69-72
    4.1.3 无序几何与图形无关证明  72-76
    4.1.4 无序几何与动态可视证明  76-77
  4.2 无序几何中的角度:全角  77-80
  4.3 基于全角法的动态可视证明自动产生方法  80-90
    4.3.1 方法的基本描述  80-83
    4.3.2 证明的层次型组织  83-85
    4.3.3 证明文本与几何图形的对应  85-86
    4.3.4 辅助元素的自动产生  86-87
    4.3.5 推导规则的可视化  87-90
  4.4 基于演绎数据库法的动态可视证明自动产生方法  90-97
    4.4.1 方法的基本描述  90
    4.4.2 证明的组织方式及其可视化  90-92
    4.4.3 演绎数据库的可视化  92-95
    4.4.4 辅助元素的自动产生  95-97
  4.5 实验结果和分析  97-98
  4.6 本章小结  98-99
第5章 JGEX的系统设计与实现  99-109
  5.1 开发历史与开发背景  99-101
  5.2 系统结构与理论基础  101-102
  5.3 JGEX的六大特性  102-106
    5.3.1 专注于平面几何  102-103
    5.3.2 支持点的轨迹  103-104
    5.3.3 基于Java  104-105
    5.3.4 基于网络  105
    5.3.5 基于代数方法  105-106
    5.3.6 动态可视证明  106
  5.4 JGEX和其它几何软件的比较  106-107
  5.5 JGEX的应用  107-108
  5.6 本章小结  108-109
第6章总结与展望  109-113
  6.1 本文的研究总结  109-110
  6.2 进一步的研究和展望  110-113
参考文献  113-120
附录  120-132
  附录一:几何定理构造形式和谓词形式  120-121
  附录二:西门松定理的8种构造形式  121-123
  附录三:伪除法  123-124
  附录四:手动输入模式中的谓词语句  124-125
  附录五:无序几何的一个例子  125-127
  附录六:全角法的推导规则  127-128
  附录七:演绎数据库法的推导规则  128-132
在学期间的研究成果  132-133
个人简历  133-134
致谢  134

相似论文

集合论等式型定理机器证明系统的研究与开发,TP181
若干逻辑自动推理方法研究,TP181
iGeo：智能几何软件的定理证明器,TP319
勾股定理研究,O124.1
出具证明编译器中证明生成的研究,TP314
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
基于树自动推理的安全协议自动化检测,TP393.08
多线程离散事件模拟语言在PVS中的建模与验证,TP311.52
一种新的基于扩展规则的知识编译方法,TP182
基于广义归结的程序综合,TP311.11
Banach空间中非线性算子半群的不动点定理和遍历理论,O177.91
交互式并行定理证明环境的构建,TP181
基于网格计算的定理自动证明研究,TP393.01
物联网传感网络安全协议形式化研究,TN915.08
设计模式的形式化研究及其EMF实现,TP311.5
高速铁路列车运行控制系统的形式化建模与验证方法研究,U270.3
用于指针逻辑的自动定理证明器的设计与实现,TP311.52
基于Chebyshev多项式零点的若干实插值问题,O174.14
安全协议分析的形式化理论与方法,TP393.04
基于扩展规则的定理证明的研究,TP301