·378 智能系统学报 第6卷 凡命题，但作为定理机器证明的一个通用程序，计算 早就被大数学家高斯(Gauss)、柯西(Cauchy)等人 复杂度仍然很高 着重研究，而哈代(Hardy)、李特尔伍德(Littlewood) 1977年吴文俊)提出的初等几何定理机器判 和波利亚(Plya)[28]、Marshall和Olkin29]及Mitrino- 定的新方法（吴方法）是这一领域的重大突破46 031]等著名数学家也相继投入探讨.可以说数学 吴方法(Wu method)主要是针对等式型命题的判定 分析，不论是纯理论还是应用，都需要不等式的运 方法.吴方法的成功在世界范围内推动了机器证明 算[321 代数方法研究的加速发展1,6,2]，但对不等式机 2007年，张福春和李姿霖发表了题为《不等式 器证明的研究仍是举步维艰，不等式机器证明的困 之基本解题方法》的论文]，系统总结了几类常用 难在于它依赖于实代数的自动推理.1996年杨路 基本不等式的证明及其应用，这些不等式包括算术 等[6,14]建立的多项式完全判别系统(a complete dis- 几何与调和平均不等式、Cauchy不等式、排序不等 crimination system for polynomials,CDS)为实代数自 式、Chebyshev不等式、Bernoulli不等式、三角形不等 动推理提供了有效的工具，使得不等式机器证明的 式及Jensen不等式等.这些不等式均依赖于离散参 成果得以普遍接受并付诸实际应用. 数n,它是一个不确定的自然数，明显属于Tarski模 自20世纪90年代以来，杨路及其团队[150]利 型外的不等式类型， 用多项式的判别序列6,41、吴方法35]和部分的柱形 本文结合不等式证明软件BOTTEMA,给出几 代数分解算法]，给出了能自动发现不等式的实 类常用的基本不等式的机器证明方法.这些不等式 用算法，这些算法对一大类不等式型定理是完备的， 包含了文献[32]中的几类基本不等式，其中，对 并在Maple下编制了通用程序BOTTEMAU15-9]和 Cauchy不等式的机器证明实现参见文献[1,23]， Discoverer].基于柱形代数分解方法的著名软件还 Bernoulli不等式针对正整数情形的机器证明实现参 有REDLOG2和QEPCADI以及Mathematica平台 见文献[1].另外，也给出文献[23-24]中所有例子 下的CAD包等.这些软件包都具有很强的实用性， 的BOTTEMA机器证明实现.这些不等式含有的变 例如，通用程序BOTTEMA已成功验证了包含上百 元个数均是任意多个，都属于Tarski模型外的不等 个公开问题的上千个代数与几何不等式，在Pentium 式类型.最后通过大量的例子来表明问题的广泛性 IV2.2GB的CPU上证明Bottema等人专著中的 及软件算法的有效性， 100个基本几何不等式2]，总共所用的CPU时间仅 应该指出，文献[32]及本文中出现的不等式， 28多口，但上述各软件所处理的问题类基本属于 均是经典的著名不等式，已有大量的相关研究，个别 Tarski模型. 不等式已有几十种甚至上百种巧妙的人工证明方 信息与科学技术及数学某些领域问题中出现的 法].本文的新意和贡献在于结合不等式证明软件 不等式有时可能会依赖于一个（甚至多个）离散参 BOTTEMA,给出这些常用基本不等式的机器证明方 数，它是一个不确定的自然数，譬如一些用传统数 法，体现机器证明的优点.机器证明方法得出的结论 学归纳法证明的命题，这类问题已经超出了Tarski 有可能推广已知的不等式，其方法本身对同类不等 的判定算法所能处理的“初等范围”，但是这类问题 式是有示范性的.当然，针对具体的不等式，可以采 并不等于不能转化为Tarski的判定算法所能处理的 用多种不同的机器证明策略，本文尽可能应用较为 “初等类型”.事实上，已经有学者借助QEPCAD 直接的策略 以及Mathematica平台下的CAD包，用计算机模拟 数学归纳法225]，文献[1]中也用B0 TTEMA证明 1常用基本不等式的机器证明 了许多以前未考虑过能用机器证明的不等式，这是 本节给出几类常用基本不等式基于不等式证明 对某些非Tarski模型命题类进行机械化证明的有启 软件BOTTEMA的机器证明过程.BOTTEMA的简易 发性的尝试.最近，文献[26-27]分别给出了实用的 使用指南山可见附录A. 算法，用于判定一类变元个数是变量的多项式正性 用B0 TTEMA证明不等式，常常仅需输入1条 和一类积分不等式命题，并在Maple平台上，根据该 (或多条)相应的BOTTEMA指令即可，为便于理解， 算法设计完成了程序，可以快速实现判定目标，这也 针对几类常用基本不等式，在给出相应BOTTEMA 属于Tarski模型外的机器可判定问题.研究讨论 指令的同时，也给出采用机器证明策略的详细分析 Tarski模型以外具有实际应用价值的机器可判定问 过程 题类是极具重要科学意义和发展前景的研究课题. 1.1算术、几何与调和平均不等式的机器证明 当今，不等式的重要应用已贯穿于当代科学技 算术、几何与调和平均不等式(arithmetic--geo 术与工程领域的多个学科分支川，不等式的理论很 metric-harmonic inequality）设a1,a2,…,a,为n个