基于吴方法的几何定理证明的恒等式方法

多年来通常认为以吴方法为代表的几何定理机器证明的坐标法给出的证明不可读,或不是图灵意义下的类人解答.其实,只要对吴氏的算法做不多的改进,即将命题的结论多项式表示为其条件多项式的线性组合,就能获得不依赖于理论、算法和大量计算过程的恒等式明证.这样的恒等式可以转化为其他更简明且更有直观几何意义的点几何形式或向量及其他形式,从而获得多种证明方法.这也证明了点几何恒等式明证方法对等式型几何命题的普遍有效性.

An identity method for proving geometry theorems based on Wu's method

For many years it was generally considered that the proofs given by the coordinate method of mechanical geometry theorem proving represented by Wu’s method were unreadable or not a humanoid solution in the Turing sense.In fact,as long as a few improvements are made to Wu’s algorithm,i.e.,expressing the conclusion polynomial as a linear combination of rational fraction coefficients of all condition polynomials,the self-evident identity proof can be obtained which is not dependent on the theory,algorithm of Wu’s method and a large number of calculation processes.Such identities can be converted to other more concise and more intuitive geometric forms,such as point geometry or vector and other forms,to obtain a variety of proving methods.This also proves the general validity of the point geometry identity method for the geometric propositions of equality type.