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

几何代数基础与质点几何的可读机器证明

作　者: 邹宇
导　师: 张景中
学　校: 广州大学
专　业: 应用数学
关键词: 几何代数质点几何可读机器证明希尔伯特交点类命题线性构造型几何命题
分类号: O187
类　型: 博士论文
年　份: 2010年
下　载: 128次
引　用: 1次
阅　读: 论文下载

内容摘要

自吴法发表至今三十余年间,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值并行方法均能有效地判定其真假,消点法、搜索法更能生成可读的证明.就几何定理可读机器证明而言,在面积法之后,又有了向量法、全角法并发展为几何代数方法和高级不变量方法.这些方法处理的主要是几何不变量而非基本的几何点,故不易于扩展和融合.且除面积法外,均尚未见形成具有完全性的算法.质点几何为发展基于几何点的几何证明方法提供了可操作的模型,其基本思想是建立几何点而不仅是坐标或不变量之间的代数运算.质点几何支持对点直接进行线性组合运算,也能表达向量和面积,其运算表达式有明显的几何意义和物理意义,是一种基本的“几何代数”.本文论证了质点几何对于几何代数的基本的重要性,并发展了一种基于几何点的几何定理可读机器证明方法——质点法,先后建立了能处理希尔伯特交点类命题和线性构造型几何命题的机器证明算法,并实现为Maple程序.由于可以直接对点进行运算,质点法的算法和编程比面积法简明.对几百个非平凡命题运行的结果显示,这种方法不仅效率高,多数证明的可读性令人满意.全文共分为五章:第一章简要回顾了几何定理可读机器证明的各种方法及几何代数的概况,并阐明了本文研究的主要目标.第二章从新视角探讨了几何代数基础.结果表明,质点几何和向量空间的出现绝非偶然,它们在某种意义上是几何代数发展过程中必然经历的一个阶段.第三章基于质点几何的基本法则,发展了能自动证明几何定理的质点几何方法,建立了能处理希尔伯特交点类命题的仿射几何机器证明算法MPM(Mass-Point-Method),并在Maple中实现为MPM证明器.第四章在质点几何的基础上,发展了复系数质点几何,基于导出的复系数质点几何的基本性质,发展了复系数质点几何方法,建立了对无序几何中可构造命题类有效的完全的算法CMPM(Complex-Mass-Point-Method),并在Maple中实现为CMPM证明器.第五章统计了410个运行例子的实验数据,总结了本文的工作,并指出了进一步研究的问题.

全文目录

中文摘要  5-6
Abstract  6-14
第一章绪论  14-26
  1.1 几何定理可读机器证明研究的历史与现状概述  14-21
    1.1.1 几何不变量方法  15-20
    1.1.2 基于数据库的搜索法  20-21
  1.2 几何代数发展概述  21-24
    1.2.1 什么是几何代数  21
    1.2.2 已有的几何代数  21-22
    1.2.3 作为几何代数的向量几何和质点几何  22-24
  1.3 本文内容概述  24-26
第二章几何代数基础新视角  26-38
  2.1 欧氏平面点集上“平等”的加法  27-28
  2.2 加法在Ω_1 上的确定  28-34
  2.3 将Ω_1 扩充为阿贝尔群  34-37
  2.4 第二章小结  37-38
第三章质点几何的可读机器证明——希尔伯特交点类命题  38-66
  3.1 实系数质点几何初步  38-47
    3.1.1 实系数质点几何的基本原理  39-41
    3.1.2 实系数质点几何解题的例子  41-44
    3.1.3 实系数质点几何的消点方法  44-47
  3.2 实系数质点几何方法描述  47-51
    3.2.1 希尔伯特交点类命题的构图语句  47-49
    3.2.2 结论的形式和检验语句  49-51
  3.3 消点算法MPM 的实现  51-58
    3.3.1 MPM 的设计思想  51
    3.3.2 MPM 的完全性  51-52
    3.3.3 MPM 的结构  52-58
  3.4 算法MPM 的Maple 实现及例子  58-63
    3.4.1 MPM的Maple实现  58-59
    3.4.2 运行希尔伯特交点类命题的例子  59-63
  3.5 第三章小结  63-66
第四章质点几何的可读机器证明——线性构造型几何命题  66-128
  4.1 复系数质点几何  66-85
    4.1.1 复系数质点几何的基本思想  66-68
    4.1.2 复系数质点几何的基本性质  68-72
    4.1.3 复系数质点几何解题的例子  72-80
    4.1.4 复系数质点几何的消点方法  80-85
  4.2 复系数质点几何方法描述  85-92
    4.2.1 线性构造型几何命题的构图语句  85-89
    4.2.2 结论的形式和检验语句  89-92
  4.3 消点算法CMPM 的实现  92-108
    4.3.1 CMPM 的设计思想  92-93
    4.3.2 CMPM 的完全性  93-94
    4.3.3 CMPM 的结构  94-108
  4.4 算法CMPM 的Maple 实现及例子  108-121
    4.4.1 CMPM 的Maple 实现  108-109
    4.4.2 运行线性构造型几何命题的例子  109-121
  4.5 算法 CMPM 与 MPM 的比较  121-124
  4.6 质点法与面积法初步比较  124-125
  4.7 第四章小结  125-128
第五章总结与展望  128-132
  5.1 总结  128-130
    5.1.1 经验数据统计  128-129
    5.1.2 本文工作总结  129-130
  5.2 进一步的问题和拟开展的工作  130-132
    5.2.1 几何代数基础方面  130
    5.2.2 基于质点几何的可读机器证明方面  130-132
参考文献  132-140
攻读博士学位期间发表的学术论文  140-141
致谢  141

几何代数基础与质点几何的可读机器证明

内容摘要

全文目录

相似论文