什么是几何定理机器证明?

[拼音]：jihe dingli jiqi zhengming

[外文]：mechanical theorem-proving in geometry

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

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

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

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

参考书目

吴文俊著：《几何定理机器证明的基本原理（初等几何部分）》，科学出版社，北京，1984。