一种几何定理机器证明的零维化方法

A Zero-Dimensional Method for Mechanical Geomery Theorm Proving

本文对一类初等几何定理的证明给出了一种机械化方法，利用这种方法，可计算出一个由有限个素理想组成的集合，所有属于假设部分对应的某一扩域上的理想的素理想都在这个集合中出现并且可以挑选出来．因而一个几何定理一般真确，当且仅当终结多项式属于全部的这种素理想，即对其不可约特征列的余式为零．

A mechanical method for proving a class of elementary geometry theorems is presented.By this method,we can obtain a set of finite prime ideals. All the prime ideals associatedwith the ideal generated by the hypothesis polynomials over an extension field appear inthis set and can be piked out.Therefore,a geometry theorem is generally true,if andonly if the conclusion polynomial belongs to each such prime ideal,i.e.,its remainders toeach irreducible characteristic set are zero.