文章以具有模型 $f(x,\tan (\frac{x}{2}))>0$ 的三角函数不等式为研究对象来探讨超越不等式的机器证明问题, 运用 Taylor 展开式将目标不等式的证明转化为一系列的一元多项式不等式的证明, 然后借助代数不等式证明工具(如 Bottema) 完成最后的工作. 运用 Maple 编制程序实现了上述算法, 实验结果表明算法对常见的三角函数不等式十分有效, 并且证明过程是``可读''的.

The problem of mechanical proving of transcendental inequalities is discussed with the trigonometric function inequalities in accordance with the model of $f(x,\tan (\frac{x}{2}))>0$ as the research object. Using Taylor expansion, the proving of the target inequality is transformed to the verification of a series of polynomial inequalities with only one variable, and then completed by algebraic inequality-proving package such as BOTTEMA. The above algorithms are implemented on Maple, and experiments show that they are very effective for most trigonometric function inequalities, furthermore the procedure is ``readable".