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

Mechanical Geometry Theorem Proving Based on the Elimination Method with Decoupling of Leading Terms for Polynomial Set

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

Using the elimination method with decoupling of leadin g terms for a polynomial set presented by the author, a polynomial set of an or iginal geometry statement of a geometry theorem can be translated into an ascend i ng polynomial set with leading coefficients without unknown variables. The nonde generate conditions without unknown variables for the original geometry statemen t can be obtained and are necessary and sufficient or nearly necessary and suff icient. Since these leading coefficients have no unknown variables, the ascendin g polynomial set is always irreducible. Therefore, the method in this paper has universal significance.