常用基本不等式的机器证明

Automated proving of some fundamental applied inequalities

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量,属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广,其方法本身对同类不等式有示范性,更多的例子表明了该算法和软件的有效性.

The automated proving of inequalities is always a difficult and hot topic in the field of intelligence systems. In this paper, by means of an inequality-proving package called BOTTEMA, the automated proving for some fundamental applied inequalities is successfully implemented. These inequalities include the arithmetic-geometric- harmonic inequality, arrangement inequality, Chebyshev inequality, Bernoulli inequality, triangle inequality, and Jensen inequality, beyond the Tarski model, where the number of variables of the inequality is also a variable. The conclusions obtained from automated proving sometimes may extend the known results; and the method would be of use for analogous types of inequalities. The effectiveness of the algorithm and package is illustrated by some more examples.