基于质点法的构造型仿射几何定理机器证明

发布时间：2017-06-14 01:17

  本文关键词：基于质点法的构造型仿射几何定理机器证明，由笔耕文化传播整理发布。

【摘要】：几何定理的机器证明是自动推理领域的热门课题之一,尤其是近些年来,研究者在研究几何定理机器证明方面取得了丰硕的成果。吴文俊先生在1997年提出了“吴法”,几何定理机器证明的研究因而取得了重大突破。通常,几何定理机器证明方法可分为代数法,人工智能法和几何不变量法三大类。代数法的优点是证明效率高,缺点是可读性差;人工智能法虽然可读性好但不完备、效率低;几何不变量法的可读性介于代数法和人工智能法之间,其证明效率与代数法也在伯仲之间。质点几何使用了比几何不变量更抽象的对象——质点,作为基本几何元素。莫绍揆先生在《质点几何学》一书中系统地阐述了质点几何的方法和理论。质点几何支持对点直接进行线性运算,在处理仿射几何问题时较为方便,为发展出一种效率更高、可读性更好的几何定理机器证明方法提供了可操作的依据。质点法是一种利用质点几何的基本原理和基本性质来证明构造型几何定理的完备性算法,具有运行效率高、可读性好、易于实现等优点。本文针对质点法生成的目标质点关系式的过程不简明,缺少明显的几何意义的问题,提出了一种具有较高可读性算法的几何定理证明器MPP。为了进一步提高质点法的可读性和证明能力,具体提出了两大改进:一个是直接使用消点公式来推导目标质点关系式,另一个是利用待定系数法来统一地判定结论质点等式的正确性。基于改进后的质点法设计了该款几何定理证明器,并采用Matlab语言实现了该证明器。由于可以对点直接进行运算,证明器MPP的消点过程比原有质点法简明,具有更加明显的几何意义。在计算机上采用Matlab语言作了10个构造型仿射几何定理的运行实验,实验结果表明该证明器具有较高的运算效率。
【关键词】：质点几何 证明器 消点法 机器证明 自动推理
【学位授予单位】：辽宁师范大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：O18;TP18
【目录】：

• 摘要4-5
• Abstract5-7
• 1 绪论7-11
• 1.1 研究背景7-8
• 1.2 研究问题及研究意义8-9
• 1.3 相关工作9
• 1.4 文章结构9-11
• 2 质点几何11-23
• 2.1 仿射质点几何11-19
• 2.1.1 仿射质点几何的基本原理11-13
• 2.1.2 仿射质点几何的解题例子13-16
• 2.1.3 仿射质点几何的消点方法16-19
• 2.2 构造型仿射质点几何命题19-20
• 2.3 质点法20-23
• 3 证明器MPP的设计23-27
• 3.1 证明器MPP的架构23
• 3.2 Loadgs模块23-25
• 3.3 Cinter模块25-26
• 3.4 Eliminition模块26
• 3.5 Solve模块26-27
• 4 证明器MPP的Matlab实现及例子27-35
• 4.1 实验数据27
• 4.2 运行构造型仿射几何定理的例子27-35
• 结论35-36
• 参考文献36-38
• 攻读硕士学位期间发表学术论文情况38-39
• 致谢39

【参考文献】

中国期刊全文数据库 前6条

1 张景中;张传军;郑焕;饶永生;邹宇;;SGARP中符号计算模块的实现及其应用[J];计算机研究与发展;2014年06期

2 邹宇;郑焕;张景中;;仿射质点几何的可读机器证明[J];计算机应用;2010年07期

3 张景中，，高小山，周咸青;基于前推法的几何信息搜索系统[J];计算机学报;1996年10期

4 张景中,杨路;定理机械化证明的数值并行法及单点例证法原理概述[J];数学的实践与认识;1989年01期

5 吴文俊;ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY[J];Science in China,Ser.A;1978年02期

6 吴文俊;初等几何判定问题与机械化证明[J];中国科学;1977年06期

  本文关键词：基于质点法的构造型仿射几何定理机器证明，由笔耕文化传播整理发布。

本文编号：448134