讨论了形如 $f(x,{\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}}_1(x),\cdots ,{\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}}_n(x))>0$的超越函数多项式不等式的自动证明问题, 运用\ Taylor 展开式将目标不等式的证明转化为一系列的一元多项式不等式的验证, 然后借助代数不等式证明工具完成最后的工作.运用 Maple实现了上述算法, 算法对常见超越函数多项式不等式十分高效, 并且可以输出``可读''的证明过程.

The problem of mechanical proving for transcendental-polynomial inequalities in accordance with the model of $f(x,{\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}}_1(x),\cdots ,{\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}}_n(x))>0$ is discussed. Using Taylor expansion, the proving of the target inequality is reduced to the verification of a series of polynomial inequalities with only one variable, and then completed by algebraic inequality-proving package. The above algorithms are implemented on Maple, and very efficient for the common transcendental-polynomial inequalities, furthermore the procedure is ``readable".