作　　者： ; ;

机构地区： 华东师范大学软件学院上海市高可信计算重点实验室

出　　处： 《智能系统学报》 2011年第5期377-390,共14页

摘　　要： 不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件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.

关 键 词： 基本不等式 机器证明 不等式证明软件 模型

领　　域： [自动化与计算机技术] [自动化与计算机技术]