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

Automated proving of some fundamental applied inequalities

作　　者：杨路[1] 郁文生[1] 

机构地区：[1]华东师范大学上海高可信计算重点实验室

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

基　　金：国家自然科学基金资助项目(61070048;60874010);国家自然科学基金委员会创新研究群体科学基金资助项目(61021004);国家"863"计划资助项目(2011AA010101);国家"973"计划资助项目(2011CB302802;2011CB302400);上海市重点学科建设资助项目(B412);上海市教育委员会科研创新资助项目(11ZZ37)

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

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

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]