第6卷第5期 智能系统学报 Vol.6 No.5 2011年10月 CAAI Transactions on Intelligent Systems 0ct.2011 doi:10.3969/i.i8gn.1673-4785.2011.05.001 常用基本不等式的机器证明 杨路，郁文生 (华东师范大学上海高可信计算重，点实验室，上海200062) 摘要：不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件B0 TTEMA,对若干常用的基 本不等式成功地实现了机器证明，包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoul山i不等 式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量，属于Tarski模型外的不等 式类型.机器证明得出的结论有时可能是已知结果的推广，其方法本身对同类不等式有示范性，更多的例子表明了 该算法和软件的有效性. 关键词：基本不等式；机器证明；不等式证明软件BOTTEMA;Tarski模型 中图分类号：TP181文献标志码：A文章编号：16734785(2011)050377-14 Automated proving of some fundamental applied inequalities YANG Lu,YU Wensheng (Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China) Abstract:The automated proving of inequalities is always a difficult and hot topic in the field of intelligence sys- tems.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. Keywords:fundamental applied inequalities;automated proving;inequality-proving package BOTTEMA;Tarski model 不等式的机器证明问题，一直是数学机械化、自 否，此种问题被称为机器（或算法）可判定的，也称 动推理及智能系统领域的研究难点和热点问题，近 为Tarski模型内的问题，该模型的任何一个确定的 年来取得了长足的进展，已有专著《不等式机器证 公式中变元的个数都是确定的有限数.但另一方面 明与自动发现》四问世.早在20世纪50年代初，波 由著名的Godel不完全性定理可知，机器可判定的 兰数学家Tarski2发表了著名的论文《初等代数与 问题类在数学中相对较少，即使在看似最简单的初 初等几何的判定方法》，证明了初等代数以及初等 等数论这一范围，其中命题的机器判定从整体而言 几何范围的命题可以用机械的步骤来判定其正确与 也是不可能实现的 对于Tarski模型内的问题，Tarski最早的判定 收稿日期：2011-04-13. 算法仅在理论上解决问题，由于其计算复杂度太高， 基金项目：国家自然科学基金资助项目(61070048,60874010)；国家 实际上不可能判定任何非平凡的代数和几何命 自然科学基金委员会创新研究群体科学基金资助项目 (61021004):国家“863”计划资助项目(2011AA010101); 题[136).后来，经Collins提出又经他人合作改进的 国家“973”计划资助项目(2011CB302802, 2011CB302400):上海市重点学科建设资助项目(B412); “柱形代数剖分(cylindrical algebraic decomposition, 上海市教育委员会科研创新资助项目(11ZZ37). CAD)”算法]，效率上有很大提高，已经能够在计 通信作者：郁文生.E-mail:wsyu@sei.ecnu.eh.cm 算机上实际判定一些难度不大的代数与几何的非平