指数多项式不等式的自动证明

Automated Proving of Exponent Polynomial Inequalities

讨论了指数多项式不等式的自动证明问题,运用Taylor展开式将目标不等式的证明转化为一系列的一元多项式不等式的验证,然后借助代数不等式证明工具(如Bottema)完成最后的工作.运用Maple实现了上述算法,算法对所有指数多项式不等式终止,并且可以输出"可读"的证明过程.

The problem of mechanical proving of exponent polynomial inequalities 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 such as Bottema. The above algo- rithms are implemented on Maple, and will terminate for all the exponent polynomial inequalities , furthermore the procedure is ＂readable＂.