基于多项式组主项解耦消元法的几何定理机器证明

基于多项式组主项解耦消元法 ,将几何定理的假设条件 (多项式组 PS)化为主项只含主变元的三角型多项式组 DTS,可得到定理命题成立的不含变元的非退化条件 ,即充分必要或更接近充分必要的非退化条件 .由于多项式主系数不含变元 ,已不存在 DTS多项式之间的约化问题 ,故方法有普遍意义 .文中例为西姆松定理的机器证明 .

Mechanical Geometry Theorem Proving Based on The Elimination Method With Decoupling of Leading Terms For Polynomial Set

Using the elimination method with decoupling of leading terms for a polynomial set presented by author, a polynomial set of an original geometry statement of a geometry theorem could be translated into a triangular polynomial set with leading coefficients without unknown variables. The nondegenerate conditions without unknown variable for the original geometry statement could be obtained and are necessary and sufficient or nearly necessary and sufficient. Since these leading coefficients have no unknown variables, the triangular polynomial set is always irreducible. Therefore, the method in this paper has universal significance.