一类三角形几何不等式的自动证明 (2012年)

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