杨路，郁文生

(华东师范大学上海高可信计算重点实验室，上海 200062)

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

杨路，郁文生

(华东师范大学上海高可信计算重点实验室，上海 200062)

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

基本不等式;机器证明;不等式证明软件BOTTEMA;Tarski模型

不等式的机器证明问题，一直是数学机械化、自动推理及智能系统领域的研究难点和热点问题，近年来取得了长足的进展，已有专著《不等式机器证明与自动发现》［1］问世.早在20世纪50年代初，波兰数学家Tarski［2］发表了著名的论文《初等代数与初等几何的判定方法》，证明了初等代数以及初等几何范围的命题可以用机械的步骤来判定其正确与否，此种问题被称为机器(或算法)可判定的，也称为Tarski模型内的问题，该模型的任何一个确定的公式中变元的个数都是确定的有限数.但另一方面由著名的G¨odel不完全性定理可知，机器可判定的问题类在数学中相对较少，即使在看似最简单的初等数论这一范围，其中命题的……