构造性和非构造性几何命题证明方法

论文摘要

定理机器证明是人工智能研究的一个重要课题,在其中的几何定理机器证明研究领域,我国的科学家最近二十几年来取得了一系列令世人瞩目的成果,提出了消点法、吴方法、几何不变量法、演绎数据库的搜索法,以及数值并行法等多种不同的方法。基于这些方法设计开发的几何定理证明系统不仅推动了人们对几何领域问题的研究,也为其它领域的定理自动证明提供了有益的启示。目前已有的几何定理证明方法大多只侧重于几何定理的严格证明,然而人们研究几何问题时会发现,除了严格证明之外,一个几何问题是否还可以用其他不怎么严格的方法来证明。有时人们感兴趣的不是它的证明过程而是证明过程中的某些几何关系。它不但有助于命题结论的证明,而且便于人们更深入透彻的理解整个几何命题,甚至可以从中发现新的未知的定理。此外,几何定理自动证明在实现方面尚有一些需要探索改进的地方,例如进一步提高证明的效率,以及解决非构造性命题等。针对这些问题,本文在数值方法的基础上提出了几何定理的动态搜索方法。在此基础上,我们结合非构造性几何命题的特点对该方法进行了改进,使其同样能够解决非构造性的初等平面几何命题,扩展了方法的应用范围。此外,我们还运用消点法证明了一些构造性和非构造几何命题,扩展了这一方法在非构造性几何命题方面的应用。

论文目录

• 摘要
• Abstract
• 引言
• 1 绪论
• 1.1 几何定理自动证明的历史和发展
• 1.2 几何定理自动证明的几种主要方法
• 1.2.1 代数方法
• 1.2.2 消点法
• 1.2.3 基于演绎数据库的方法
• 1.3 研究现状和本文的工作
• 2 几何定理证明的数值方法
• 2.1 引言
• 2.2 数值并行法基本原理
• 2.3 单点实验法基本原理
• 2.4 小结
• 3 基于数值计算的几何定理动态搜索方法
• 3.1 引言
• 3.2 方法概述
• 3.2.1 定理预搜索
• 3.2.2 定理动态搜索
• 3.2.2.1 动态搜索的方法
• 3.2.2.2 基于自由点构造新的几何对象
• 3.2.2.3 定理动态搜索过程的描述
• 3.3 小结
• 4 几何定理动态搜索方法解决非构造性命题
• 4.1 引言
• 4.2 解决非构造性问题
• 4.2.1 非构造性问题条件输入
• 4.2.2 非构造性问题构造化
• 4.2.3 非构造性命题动态搜索过程
• 4.3 小结
• 5 消点算法及证明实例
• 5.1 引言
• 5.2 预备知识
• 5.2.1 有向线段
• 5.2.2 带号面积
• 5.2.3 勾股差
• 5.3 消点算法的具体要素，步骤和公式
• 5.4 消点法证明构造性和非构造性几何命题实例
• 5.5 小结
• 6 结论
• 6.1 本文的工作意义
• 6.2 今后的研究方向
• 参考文献
• 在学研究成果
• 致谢