基于数值计算的几何定理动态搜索方法的研究与实现

摘要

定理机器证明是人工智能研究的一个重要课题。在其中的几何定理机器证明研究领域，我国的科学家最近二十几年来取得了一系列令世人瞩目的成果，提出了吴方法、几何不变量法、演绎数据库的搜索法，以及数值并行法等多种不同的方法。基于这些方法设计开发的几何定理证明系统不仅推动了人们对几何领域问题的研究，也为其它领域的定理自动证明提供了有益的启示。 目前已有的几何定理证明方法大多只侧重于几何定理的严格证明，然而人们研究几何问题时会发现，除了命题给出的结论外，一个几何问题往往还包含很多其它有意义的信息。有时挖掘出人们感兴趣的某些几何关系的有用信息不但有助于命题结论的证明，而且便于人们更深入透彻的理解一个几何命题，甚至可以从中发现新的未知的定理。 已有的方法中，基于演绎数据库的搜索方法虽然可以在证明命题时搜索出其它有用的几何信息，但是该方法为了证明命题的结论而采用“大英博物馆”式的推理方法，使中间几何信息过度膨胀，也影响了证明命题的效率。因此，如果能够找到一个更高效的定理证明方法，可以在证明定理的同时对人为指定的几何关系进行全面的信息搜索，找出人们关心的几何关系所有成立的结论信息，无疑有助于我们更快捷方便的研究和解决几何问题。 此外，几何定理自动证明在实现方面还尚有一些需要探索改进的地方，例如进一步提高证明的效率，以及解决非构造性命题等。 针对这些问题，本文在数值方法的基础上提出了几何定理的动态搜索方法，能够在证明初等平面几何命题的同时，快速全面的对该命题进行定理信息搜索。该方法采用不同于传统严格的证明方法，而是在搜索的过程中通过随机举例的方法证明结论是否成立，因此效率要比人工智能推理的方法有很大提高。国外这一领域最新的研究结果表明，概率意义上的验证方法能够保证最终结论正确的概率高达1-ε，因此几何定理动态搜索方法能够快速将绝大部分错误信息排除，并且所有正确的信息都包含在最终搜索的信息集合中。 在此基础上，我们结合非构造性几何命题的特点对该方法进一步改进，使其同样能够解决非构造性的初等平面几何命题。扩展了方法的应用范围。 本文研究方法的同时，在Windows平台上使用VisualC++和Matlab编程工具，对涉及的算法进行了系统的开发和实现，设计了几何定理动态搜索测试系统。在已实现算法的几何谓词基础上，该系统可以高效的搜索和证明仅涉及这些谓词的初等平面几何定理，其中也包括一些非构造性的几何命题，充分证明了本文方法的有效性。

目录

学位论文独创性声明及学位论文使用授权声明

摘要

第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数值计算的误差问题

§2.5小结

第3章基于数值计算的几何定理动态搜索方法

§3.1引言

§3.2方法概述

§3.2.1定理预搜索

§3.2.2定理动态搜索

§3.3结论信息的正确性问题

§3.4方法的改进

§3.4.1效率优化问题

§3.4.2信息压缩问题

§3.5小结

第4章几何定理动态搜索方法解决非构造性命题

§4.1引言

§4.2解决非构造性问题

§4.2.1非构造性问题条件输入

§4.2.2非构造性问题构造化

§4.2.3非构造性问题动态搜索

§4.3小结

第5章系统设计与实现

§5.1系统设计基础

§5.1.1谓词选取与实现

§5.1.2类的定义

§5.2系统结构

§5.2.1系统模型

§5.2.2系统流程图

§5.3系统工作过程

§5.3.1动态作图

§5.3.2生成题目

§5.3.3定理信息搜索

§5.3.4搜索结论输出

§5.4非构造性问题的解决

§5.4.1非构造性问题处理流程图

§5.4.2生成非构造性图形

§5.4.3信息搜索与输出

§5.5系统应用实例

§5.6小结

第6章系统开发工具与环境

§6.1基于VISUAL C++的面向对象编程方法

§6.3.1运用MCC将Matlab的代码编译为VC编译器能识别的代码

§6.3.2利用Matlab引擎

§6.3.3使用Matcom技术

§6.4方法比较

§6.5 MATLAB计算引擎在几何定理动态搜索系统中的应用

§6.6一个重要函数的介绍

第7章结论

§7.1本文的工作意义

§7.2今后的研究方向

参考文献

附录

致谢