三角函数不等式的自动证明

Automated proving of trigonometric inequalities

本文以三角函数不等式为研究对象来探讨超越不等式的机器证明问题,运用变量替换和函数的Taylor展开式将目标不等式代数化,然后借助BOTTEMA中强有力的代数不等式证明工具完成最后的证明.编制程序实现了上述算法,实验结果表明算法对常见的三角函数不等式十分有效,并且算法是"可读"的.

The problem of mechanical proving about transcendental inequalities is discussed with the trigonometric inequalities as the research object. Using variable substitution and Taylor expansion,the target inequality is transformed to an algebraic one, and then proved by the powerful inequality-proving package BOTTEMA. The above algorithms are implemented on Maple,and experiments show that they are very effective for most trigonometric inequalities, furthermore the procedure is ＂readable＂.