一类初等几何定理的机械化证明

Mechanical Demonstration for a Class of Elementary Geometric Theorems

对一类初等几何定理，通过根理想的分解，给出了一种机械化方法，利用这种方法，可恰好同时获得所有的不可约特征列．因而一类几何定理是一般真确的当且仅当其终结多项式对这些不可约特征列的余式为零．

By decomposing a radical ideal, a method can be given to obtain all the useful irreducible characteristic sets. Then, a geometric theorem is generally true if the remainders of the conclusion polynomial to these characteristic sets are zero.