智能系统学报2011，Vol.6Issue(5)：377-390,14.DOI:10.3969/j.issn.1673-4785.2011.05.001
常用基本不等式的机器证明
Automated proving of some fundamental applied inequalities
摘要
Abstract
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模型Key words
fundamental applied inequalities/ automated proving/ inequality-proving package BOTTEMA/ Tarski model分类
信息技术与安全科学引用本文复制引用
杨路,郁文生..常用基本不等式的机器证明[J].智能系统学报,2011,6(5):377-390,14.基金项目
国家自然科学基金资助项目(61070048,60874010) （61070048,60874010）
国家自然科学基金委员会创新研究群体科学基金资助项目(61021004) （61021004）
国家"863"计划资助项目(2011AA010101) （2011AA010101）
国家"973"计划资助项目(2011CB302802,2011 CB302400) （2011CB302802,2011 CB302400）
上海市重点学科建设资助项目(B412) （B412）
上海市教育委员会科研创新资助项目(11ZZ37). （11ZZ37）
