jihe dingli jiqi zhengming 几何定理机器证明 mechanical theorem-proving in geometry 用计算机自动证明某一类型几何定理，甚至某一种几何全部定理的原理和方法。从理论角度看，几何定理的机器证明要经历公理化、代数化与坐标化、机械化等步骤，才能编制程序并在计算机上实现。可用机器证明的几何定理(主要是初等几何的定理)有三种不同类型，与之对应则有三种不同的机器证明方法。每一类型定理的机器证明都必须假设代数化与坐标化已经完成，而且可把几何定理的证明问题化为一些代数关系式的处理问题。

中文名

几何定理机器证明外文名

mechanical theorem-proving in geometry

所属学科

几何定理机器证明类型

编辑

语音

几何定理机器证明①第一类型

定理的特征是假设部分的所有代数关系式对于某些特定变量都必须是线性的，包括一类构造型的纯交点定理，其对应的机器证明方法称为希尔伯特方法；

几何定理机器证明②第二类型定理

特征是假设和终结部分的代数关系式都可用多项式的方程来表示，其对应的机器证明方法是中国数学家吴文俊首先提出的,称为吴文俊方法;

几何定理机器证明③第三类型定理

特征是假设和终结部分可以是任意的多项式等式或不等式，但其系数必须在一实闭域中，因而原来的几何必须有次序关系，其对应的机器证明方法称为塔斯基方法。这三种方法各有其适用范围，但就可以通用的那些定理证明问题来说，希尔伯特法效率最高而塔斯基法效率最低，但是前者的适用范围很窄。1980年在 HP9835A机上，用吴文俊方法成功地证明了勾股定理、西姆逊线定理、帕普斯定理、帕斯卡定理、费尔巴哈定理,并在45个帕斯卡点中发现了20条帕斯卡圆锥曲线,这种方法还推广到微分几何，将微分几何曲线论中的贝屈朗定理推广到仿射微分几何。吴文俊的研究成果引起了国际学术界的重视。

几何定理机器证明几何定理机器证明的几种主要方法

编辑

语音

几何定理机器证明代数方法

几何定理机器证明的代数方法又包含多种不同的方法，如吴方法、Grobner 基方法、单点例证法、数值并行法等。其中，吴方法是代数方法的代表，其它几种方法都是在吴方法之后，受其思想的影响提出来的。吴方法是我国著名数学家吴文俊先生1977年提出来的一种用代数的方法来证明几何定理的新的方法。该方法适用于证明“等式型”的几何定理，而且证明的效率很高，一般可以用几分钟甚至几秒钟就可以证出不简单的定理。其中，等式型几何定理是指：将几何问题引进坐标化为代数问题后，问题的条件和结论都可以化为若干个等式的形式。

吴方法进行几何定理机器证明的第一步是几何问题代数化，建立坐标系，并将命题涉及的几何图形的点选取适当的坐标，然后把命题的条件和结论表示为坐标的多项式方程组。最后判断条件方程组的解是否满足结论方程。通常的几何命题涉及的多项式方程组都是非线形的，一般无法将约束变元求出。吴方法是利用伪除法判定条件方程组的解是否是结论方程组的解。而且利用吴方法不仅可以判断定理的正确与否，还可以自动找出定理赖以成立的非退化条件，这是传统的做法无法做到的。多项式的伪余除法可以通过计算机做符号计算进行。此外，单点例证法和数值并行法，这两种方法与吴方法进行大量符号计算不同，主要利用数值计算的方法进行定理的证明，所以有时也被单独列为一类方法，即几何定理证明的数值方法。数值方法与其它方法相比，具有效率高的优点。

几何定理机器证明几何不变量

以吴方法为代表的代数方法仅仅能够判断几何命题的成立与否，证明的过程十分复杂，而且需要进行大量的数值计算和符号计算，这与传统几何证明的简洁明了大相径庭。人们难以读懂这种方法生成的证明，往往只能得出命题真假的结论，因此很多人难以接受这种证明的风格。如何生成让人容易读懂的几何证明过程这一问题成为科学家面临的又一个严峻的挑战。 1992年，中科院院士张景中教授以其多年研究的面积法为基础，提出了几何定理机器证明的新方法，基于几何不变量的消点法。随后，它与周咸青、高小山合作完善了该方法，并编写了程序，终于成功的利用计算机对大量非平凡的几何命题生成了简洁易读的几何证明，这一杰出的工作被誉为计算机处理几何问题的里程碑。 消点法包括一组构图规则、一组几何不变量以及一组消点公式。该方法的基本思想是：利用构图规则将欲证几何命题中涉及的图形构造出来，并在构图的过程中生成关于点的约束条件，同时将欲求证的命题表示成图中几何量的等式的形式，然后利用消点公式，按照点在作图时出现的相反顺序，依次从结论等式中消去，最终结论等式会化为显然成立的等式。后来，杨路教授又将消点法拓展到非欧几何，成功的证明和发现了大量的新的非欧几何定理。李洪波博士、杨海圈博士也在面积不变量的基础上提出用向量法实现几何定理的可读证明，即Clifford代数法，也取得了很好的效果。

几何定理机器证明基于演绎数据库的搜索法

几何不变量的方法虽然实现了一大类几何定理的机器的可读证明，但是这种方法得到的证明过程常常不符合人的思维习惯。而利用演绎数据库的方法，根据几何命题所给的条件、已知的公理、定理及公式等推理规则，通过大量的试验匹配的方法进行证明似乎更符合人的思维习惯。这种方法也被誉为“大英博物馆式的推理方法”，最早有这种设想的是H.Gelernter,J.R.Hanson和D.W.Loveland。它们于1960年联合发表一篇文章中提出了从结论出发进行搜索的后推链方法。

几何定理机器证明进展

编辑

语音

到了1975年，A.J.Nevins又提出了前推链方法，但是仍不能实现为有效的算法和程序。随后的几十年里，科学家基于这两种推理设想进行了大量的探索，但始终收效不大。直到1996年，张景中、高小山、周咸青提出了一个基于前推模式的“几何信息搜索系统” (GISS)，成功的证明了161个非平凡的几何命题，收到了良好的效果。基于该方法进行了较多的研究，也成功设计了一些的定理证明系统，取得了不错的效果。演绎数据库方法的特点是：不仅给出了定理的证明，还可以生成一个几何性质的数据库。该数据库包含了所给几何图形中能由系统内部所用几何公理推导出来的所有几何性质。例如：证明垂心定理，最终数据库中包含下面的几何信息——6个共线关系，6个共圆关系，24个等角关系，7个三角形相似关系，105个等比关系。可见得到的信息十分丰富，但是这也成为这种方法的一个瓶颈，即中间的几何信息过度膨胀。因此针对这一问题进行了大量的改进。

词条图册

更多图册