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