一类三角形几何不等式的自动证明

Automated proving for class of triangle geometric inequalities

讨论了一类只含三角函数的三角形几何不等式的自动证明问题。运用代数方法将其有理化,在不新增加根式的条件下将问题转换为一个二元多项式不等式的证明,设计的基于胞腔分解和实根分离的算法实现了二元多项式不等式的自动证明,输出的证明过程可以手工验证或借助一些数学软件进行理解。实验表明上述算法对一大批具有相当难度,特别是关于三角函数的几何不等式十分高效,并且能够解决三角形内角的任意有理倍数函数的不等式机器证明问题。

This paper discussed the automated proving for a class of triangle geometric inequalities with only trigonometric functions.Without new radicals,it firstly transformed the original inequality to a two-variable polynomial one using algebraic method firstly.And then it implemented an algorithm based on cell decomposition and real root isolation to prove the two-variable polynomial inequalities,and the output was readable or could be understood with the help of mathematic software.Experiments show that the above methods can prove an extensive class of geometric inequalities with great difficulty automatically and are much efficient especially for the inequalities with only trigonometric functions.Furthermore,the algorithm is suit for triangle geometric inequalities with arbitrary rational coefficients of interior angles.