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

杨路，郁文生

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

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

杨路，郁文生

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

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

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

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

对于Tarski模型内的问题，Tarski最早的判定算法仅在理论上解决问题，由于其计算复杂度太高，实际上不可能判定任何非平凡的代数和几何命题［1，3－6］.后来，经 Collins 提出又经他人合作改进的“柱形代数剖分(cylindrical algebraic decomposition，CAD)”算法［7－11］，效率上有很大提高，已经能够在计算机上实际判定一些难度不大的代数与几何的非平凡命题，但作为定理机器证明的一个通用程序，计算复杂度仍然很高.

1977年吴文俊［3］提出的初等几何定理机器判定的新方法(吴方法)是这一领域的重大突破［4－6］.吴方法(Wu method)主要是针对等式型命题的判定方法.吴方法的成功在世界范围内推动了机器证明代数方法研究的加速发展［1，4－6，12－13］，但对不等式机器证明的研究仍是举步维艰，不等式机器证明的困难在于它依赖于实代数的自动推理.1996年杨路等［6，14］建立的多项式完全判别系统(a complete discrimination system for polynomials，CDS)为实代数自动推理提供了有效的工具，使得不等式机器证明的成果得以普遍接受并付诸实际应用.

自20 世纪 90 年代以来，杨路及其团队［15－20］利用多项式的判别序列［6，14］、吴方法［3－5］和部分的柱形代数分解算法［7－11］，给出了能自动发现不等式的实用算法，这些算法对一大类不等式型定理是完备的，并在 Maple 下编制了通用程序 BOTTEMA［15－19］和Discoverer［20］.基于柱形代数分解方法的著名软件还有 REDLOG［21］和 QEPCAD［11］以及 Mathematica 平台下的CAD包等.这些软件包都具有很强的实用性，例如，通用程序BOTTEMA已成功验证了包含上百个公开问题的上千个代数与几何不等式，在Pentium IV 2.2 GB的CPU上证明Bottema等人专著中的100个基本几何不等式［22］，总共所用的CPU时间仅2 s多［1］，但上述各软件所处理的问题类基本属于Tarski模型.

信息与科学技术及数学某些领域问题中出现的不等式有时可能会依赖于一个(甚至多个)离散参数n，它是一个不确定的自然数，譬如一些用传统数学归纳法证明的命题，这类问题已经超出了Tarski的判定算法所能处理的“初等范围”，但是这类问题并不等于不能转化为Tarski的判定算法所能处理的“初等类型”.事实上，已经有学者借助 QEPCAD［11］以及Mathematica平台下的CAD包，用计算机模拟数学归纳法［23－25］，文献［1］中也用 BOTTEMA 证明了许多以前未考虑过能用机器证明的不等式，这是对某些非Tarski模型命题类进行机械化证明的有启发性的尝试.最近，文献［26－27］分别给出了实用的算法，用于判定一类变元个数是变量的多项式正性和一类积分不等式命题，并在Maple平台上，根据该算法设计完成了程序，可以快速实现判定目标，这也属于Tarski模型外的机器可判定问题.研究讨论Tarski模型以外具有实际应用价值的机器可判定问题类是极具重要科学意义和发展前景的研究课题.

当今，不等式的重要应用已贯穿于当代科学技术与工程领域的多个学科分支［1］.不等式的理论很早就被大数学家高斯(Gauss)、柯西(Cauchy)等人着重研究，而哈代(Hardy)、李特尔伍德(Littlewood)和波利亚(Pólya)［28］、Marshall和 Olkin［29］及 Mitrinovi［30－31］等著名数学家也相继投入探讨.可以说数学分析，不论是纯理论还是应用，都需要不等式的运算［32］.

2007年，张福春和李姿霖发表了题为《不等式之基本解题方法》的论文［32］，系统总结了几类常用基本不等式的证明及其应用，这些不等式包括算术、几何与调和平均不等式、Cauchy不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.这些不等式均依赖于离散参数n，它是一个不确定的自然数，明显属于Tarski模型外的不等式类型.

本文结合不等式证明软件BOTTEMA，给出几类常用的基本不等式的机器证明方法.这些不等式包含了文献［32］中的几类基本不等式，其中，对Cauchy不等式的机器证明实现参见文献［1，23］，Bernoulli不等式针对正整数情形的机器证明实现参见文献［1］.另外，也给出文献［23－24］中所有例子的BOTTEMA机器证明实现.这些不等式含有的变元个数均是任意多个，都属于Tarski模型外的不等式类型.最后通过大量的例子来表明问题的广泛性及软件算法的有效性.

应该指出，文献［32］及本文中出现的不等式，均是经典的著名不等式，已有大量的相关研究，个别不等式已有几十种甚至上百种巧妙的人工证明方法［33］.本文的新意和贡献在于结合不等式证明软件BOTTEMA，给出这些常用基本不等式的机器证明方法，体现机器证明的优点.机器证明方法得出的结论有可能推广已知的不等式，其方法本身对同类不等式是有示范性的.当然，针对具体的不等式，可以采用多种不同的机器证明策略，本文尽可能应用较为直接的策略.

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

本节给出几类常用基本不等式基于不等式证明软件BOTTEMA的机器证明过程.BOTTEMA的简易使用指南［1］可见附录A.

用BOTTEMA证明不等式，常常仅需输入1条(或多条)相应的BOTTEMA指令即可，为便于理解，针对几类常用基本不等式，在给出相应BOTTEMA指令的同时，也给出采用机器证明策略的详细分析过程.

1.1 算术、几何与调和平均不等式的机器证明

算术、几何与调和平均不等式(arithmetic－geometric－harmonic inequality) 设 a1，a2，…，an为 n 个正实数，则

显然，仅需对n个正实数a1，a2，…，an，证明如下的算术与几何平均不等式:

将式(2)取倒数即得

下面给出式(1)的证明.容易验证式(1)在n=1时成立.按照数学归纳法，假设式(1)成立，则需要证明

亦成立.由于式(1)成立，只需证

上式可以改写成:

现在，仅需证明式(5)对任意正数x和任意正整数n成立即可.仍用数学归纳法，记式(5)为φn，显然φ1成立.为证

这时引进新的变元r，考虑命题:

如果式(7)为真，那么式(6)当然就为真，因为可以令r代表xn.由于r、x、n全都是非负，因此可以执行BOTTEMA的xprove指令:

(n+2)*r*x，［n*r*x+1＞=(n+1)*r］);屏幕几乎立即提示“The inequalitity holds”.这即完成了算术几何平均不等式的证明.

对于算术与几何平均不等式(1)的机器证明，还可以采取多种其他不同的策略，例如，容易知道，算术与几何平均不等式(1)等价于如下的Jacobsthal不等式［33］:

(n+1)*s*a*b，［(n－1)*s*a+t＞=n*s*b］);屏幕几乎立即提示“The inequalitity holds”.

对于几何与调和平均不等式(3)，也可仿照上述过程给出其机器证明方法，当然，直接利用算术与几何平均不等式(1)证明几何与调和平均不等式(3)的过程也是非常简单的.

如果考虑如下的算术与调和平均不等式:

类似上面的讨论，引进新变元A、B，执行BOTTEMA的xprove指令:

即完成了式(9)的机器证明.

1.2 Cauchy不等式的机器证明

Cauchy不等式(Cauchy inequality) 设x1，x2，…，xn及y1，y2，…，yn为 2 组实数数列，则

该不等式的机器证明实现参见文献［1，23］，文献［23］基于 QEPCAD［11］，而文献［1］是基于 BOTTEMA的.下面采用文献［1］的方法，记φn是如下公式:

容易验证φ1和φ2成立.按照数学归纳法，需要证明

这时引进新的变元r、s、t、x、y，考虑命题:

注意，式(11)是一个实量词消去问题［11］，因而它是否为真是可以判定的.譬如，可以执行BOTTEMA的yprove指令:

屏幕几乎立即提示“The inequalitity does not hold”，即该命题一般不为真.

不过显而易见，如果已经证明Cauchy不等式对于所有的xk≥0，yk≥0 成立，那么当xk、yk为一般实数时它也必然成立.这样不妨假设xk、yk非负，从而r、s、t全都是非负的.于是可以执行 BOTTEMA的xprove指令:

经大约 0.05 s之后屏幕提示“The inequalitity holds”，这即完成了Cauchy不等式的证明.

1.3 排序不等式的机器证明

排序不等式(arrangement inequality) 设有2组实数有序数列a1≤a2≤…≤an及b1≤b2≤…≤bn，则

式中:j1，j2，…，jn是 1，2，…，n的任一排序.

排序不等式可以导出许多不等式，例如算术与几何平均不等式、Cauchy不等式及下一小节的Chebyshev不等式等.

先证明“顺序和大于等于乱序和”.令S=akbjk，不妨假设S中jn≠n(若jn=n则考虑jn－1)，则在S中存在某个m≠n，使得bn与am搭配，即在S中含有项ambn(m≠n).因此，只要

成立，即表明当jn≠n时，调换S中bn和bjn的位置(其余n－2项保持不变)，会使S增加.同理可证其他ak必须和bk搭配(k=1，2，…，n－1).

为证式(12)，只需执行BOTTEMA的yprove指令:

即可得证.事实上，式(12)亦容易从下式中直接得到［32－33］.

这里调用BOTTEMA的yprove指令，只是为了说明本文机器证明方法的统一性.这即完成了“顺序和大于等于乱序和”的证明.

仿照上述过程可以给出“乱序和大于等于逆序和”的机器证明，当然，也可直接利用“顺序和大于等于乱序和”来证明“乱序和大于等于逆序和”，这只需对2组实数a1≤a2≤…≤an及 －bn≤ －bn－1≤…≤－b1应用“顺序和大于等于乱序和”即可.这样即完成了排序不等式的证明.

1.4 Chebyshev不等式的机器证明

Chebyshev不等式(Chebyshev inequality) 设a1≤a2≤…≤an及b1≤b2≤…≤bn为两递增实数列，则

Chebyshev不等式当然可以由排序不等式证得，下面给出基于BOTTEMA的证明方法.为使机器证明更好地体现Chebyshev不等式前提中的单调性条件，引进比“单调数列”更广泛的所谓“均和单调数列”的概念.

定义1 给定数列{ai，i=1，2，…}，若满足条件:

则称该数列是均和不减的;若上式中的不等号反向成立，则称该数列是均和不增的;若不等式严格成立，则称该数列是均和递增(递减)的.

显然，单调递增的数列是均和不减的，单调递减的数列是均和不增的.

先证

注意到“均和单调数列”的定义，只需执行BOTTEMA的yprove指令:

为证

式(14)即可得证.

这样即完成了Chebyshev不等式的机器证明.事实上，这就已经证明Chebyshev不等式对于均和单调的数列都是成立的，这已经在一定程度上推广了原来的Chebyshev不等式类型.

对于上面通过BOTTEMA指令yprove证明的2个命题，还有另一种较简单的，甚至可认为是机器明证(certificate)［1］的方法，也是富有启发性的，在同类问题的机器证明中可能会有效.这里也简单介绍它的证明过程如下.

命题 1若rs≤nt，nx≥r，ny≥s，n≥1，则

证明根据题设，不妨令

式中:w≥0，p≥0，q≥0，将式(16)代入

化简整理得

式(17)显然是非负的，于是式(15)成立，命题1得证.

类似地，可以证明如下的命题.

命题 2若rs≥nt，nx≥r，ny≤s，n≥1，则

证明根据题设，不妨令

式中:w≥0，p≥0，q≥0，将式(19)代入

化简整理，得

式(20)显然是非负的，于是式(18)成立，命题2得证.

命题1和命题2的证明根本无需BOTTEMA，在任何符号计算软件平台上都容易验证.

1.5 Bernoulli不等式的机器证明

Bernoulli不等式(Bernoulli inequality) 设a＞ －1，且r≥1 或r≤0，则

若r的范围为(0，1)，则有

成立.

1)Bernoulli不等式(21)针对r取正整数情形的机器证明实现参见文献［1］.事实上，式(21)在r=1时成立.记x=a+1，A=xn，归纳步骤变成证明

使用BOTTEMA的xprove指令:可在不到1 s的时间内证明式(21)成立.

2)对于Bernoulli不等式(21)中r取负整数的情形，此时式(21)在r=0时成立.记x=a+1，A=x－n，归纳步骤变成证明

使用BOTTEMA的xprove指令:

同样可在不到1 s的时间内证明式(21)成立.

使用BOTTEMA的xprove指令:

同样可在不到1 s的时间内证明式(22)成立.

于是，使用BOTTEMA的xprove指令:

使用BOTTEMA的xprove指令:

最后，对于Bernoulli不等式(21)或(22)在r取任意实数的情形，可由有理数在实数中的稠密性和指数函数的连续性，再结合上面的诸结论得到，这样即完成了Bernoulli不等式的机器证明.

1.6 三角形不等式的机器证明

三角形不等式(triangle inequality) 设a=(a1，a2，…，an)和 b=(b1，b2，…，bn)为 2 个向量，则

从几何角度看，式(23)右边不等式即三角形中任意两边长的和大于第三边长，式(23)左边不等式即三角形中任意两边长的差小于第三边长.

三角不等式当然可以由Cauchy不等式证得.下面给出基于BOTTEMA的证明方法，根据向量模的定义，即是要证明

先证式(24)右边的不等式，易见，此时不等式若对所有的ak≥0，bk≥0成立，那么当ak、bk为一般实数时它也必然成立.这样只需执行BOTTEMA的xprove指令:

对于式(24)左边的不等式，可以对c=a+b和d=－b应用式(24)右边的不等式即可，也可以类似于式(24)右边不等式的机器证明，执行BOTTEMA的xprove指令:

即可得证.这样就完成了三角形不等式的机器证明.

1.7 Jensen不等式的机器证明

Jensen不等式(Jensen inequality) 设函数f在区间I⊆R 上为一凸函数，a1，a2，…，an∈I且 0 ＜t1＜t2＜…＜tn＜1，=1，则

若f为一凹函数，则将式(25)的不等式变号.

这里为明确起见，给出凸函数与凹函数的定义如下.

定义2函数f称为在区间I⊆R上的凸函数，若满足a1，a2∈I，0 ＜ λ ＜1，且

若将式(26)的不等式变号，则f即为凹函数.

同理，若f为凹函数，则将式(27)的不等式变号.

Jensen不等式当然可用数学归纳法直接得证［32］.下面给出迂回的代换方法，本质上与文献［32］的方法相同，只是为了说明在机器证明不等式的过程中，如何处理像Jensen不等式这样含有未具体给出明确定义的函数f的情形，这也是为了说明机器证明方法的统一性.

利用数学归纳法.由定义2知Jensen不等式在n=2时成立.若假设Jensen不等式在n=k时成立，考察n=k+1的情形，作如下代换:

于是，自然有

上式当然也可通过执行BOTTEMA的yprove指令:

(1－t)*B+t*C，B＜=D，t＞0，1－t＞0］);从而得证.

2 更多的实例

本节提供更多的具有典型意义的不等式机器证明的例子，包括文献［23－24］中所有例子的BOTTEMA机器证明实现.为完整起见，列出文献［1］中已经用BOTTEMA机器证明实现的几个典型例子.需要说明的是，对于文献［23－24］中的例子，当时作者是借助QEPCAD［11］以及Mathematica平台下的CAD包给出其机器证明的，并特别指出这些例子以前从未被机器自动证明过，但可以看到，这些例子基于BOTTEMA机器证明实现时，可能更为方便简洁.

例 1［1，23］证明文献［30］中的一个不等式:

显然n=1时上式成立.记上式左端为r，归纳步骤变成证明

使用BOTTEMA的xprove指令:

可在几秒内证明上式成立.

例 2［1］证明

对一切满足下列条件的实数xk、yk成立.

这个所要证明的不等式称为Aczél不等式，可以看作是Cauchy不等式的双曲版本，在非欧几何中有应用，它首先是由 Aczél等提出并证明的［34－35］.

显然只要证明该不等式对于一切正数xk、yk成立就够了，所以仍用BOTTEMA的xprove指令来完成如下归纳步骤:

执行指令:

BOTTEMA在验证了1 156个样本点后证明了Aczél不等式.

例 3［1，24］用机器证明 Turán 不等式:

式中:Pn(x)表示第n个Legendre多项式.

首先，因为P0(x)=1，P1(x)=x，P2(x)=(3x2－1)/2，所以容易验证不等式在n=1时成立.其次，考虑归纳步骤:

如果把Pn－1、Pn、Pn+1、Pn+2分别命名为Y－1、Y0、Y1、Y2，则式(28)变成量词消去问题:

式(29)显然为假，于是需要添加一些条件.根据Legendre多项式的递归性质:

那么，修改后的量词消去问题变为:

这个命题的假设条件中包括2个等式，必须通过降维(消元)去掉等号后才能应用BOTTEMA程序.根据这2个等式消去变量Y1、Y2之后，得到一个仅含有4个变量X、Y0、Y－1、N的新命题.该命题可以用 yprove 指令在几秒钟内证明成立，即完成了归纳证明.

例 4［23］证明

计算机耗时不足1 s即证明式(30)成立.这里之所以用2条xprove指令，是因为分别考虑了当n为奇数或偶数时的递推.

例5［23］证明文献［30］中3.27的一个不等式:

式中:是寻常的二项系数，即

为证式(31)右端的不等式，使用 BOTTEMA的xprove指令:

计算机耗时不足1 s即能证明式(31)成立.

例6［23］证明文献［31］中3.2.12所谓的Levin不等式:

式(32)左端的不等式已在证明算术几何平均不等式的过程中完成，只需执行 BOTTEMA的xprove指令:

为证式(32)右端的不等式，执行 BOTTEMA的xprove指令:

计算机耗时不足1s即证明式(32)成立.

例7［23］证明文献［31］中3.3.38的递推不等式，若记Fn(x)为第n个Fibonacci多项式，其递推定义如下:

式中:R表示实数集合.

显然式(33)在n=3和n=4时成立.记Y1=Fn(x)，Y2=Fn+1，A=(x2+2)n－3，使用 BOTTEMA的yprove指令:

计算机在2 s内即能证明式(33)成立.

例8［23］证明文献［36］中的定义的如下递推公式:

显然式(34)在n=3成立.分别执行BOTTEMA的xprove指令:

计算机耗时不足1 s能证明式(34)成立.

例9［23］证明文献［30］中4.15的一个相关不等式:

显然式(35)在n=1时成立.记A=，执行BOTTEMA的xprove指令:

计算机在2 s内证明式(35)成立.

例10［23］证明文献［31］中第112页Thm.6的一个不等式:

式中:(ak)k≥1是正的递减的序列.

显然式(36)在n=1时成立.记

使用BOTTEMA的xprove指令:

［A－a2＞=(B－a)2，A＞B2，a＞=b］);计算机耗时不足1 s即能证明式(36)成立.这里之所以用2条xprove指令，是因为分别考虑了当n为奇数或偶数时的递推.

例11［23］证明文献［30］中7.31与7.32出现的相关不等式:

式中:xk＞0，x2＞4x1，n≥2.

显然式(37)在n=2时成立.记

对于式(37)中的第1个不等式，执行BOTTEMA的xprove指令:

对于式(37)中的第2个不等式，执行BOTTEMA的xprove指令:

计算机耗时不足1 s即能证明式(37)成立.事实上，式(37)中的第2个不等式不用机器证明，可直接由下面显然成立的不等式得到.

例12［23］证明文献［31］中 3.2.37所谓的Weierstrass不等式:

式中:n≥1，0＜a＜1且＜1.

k

显然式(38)和式(39)在n=1时成立.记

依次执行如下BOTTEMA的xprove指令:

计算机耗时不足1 s即能证明式(38)和(39)成立.

例13［23］考虑文献［37］中的不等式(文献［23］在给出式(40)时有一个明显的打印错误，将式(40)左端x的一个下标k误印为i了):

式中:xk＞0，α≥1且α+β≥1.该不等式对于确定的α和β是可以机器证明的.下面给出α=2，β=－1情形的证明.

例14［23］考虑文献［30］中5.16的不等式:

式(41)在n确定时就是普通的三角不等式，文献［30］中验证了n=1，2，3，4 的情形.在处理三角不等式时，BOTTEMA具有极高的效率，例如，即使取n=90，依然可以执行BOTTEMA的prove指令:

计算机在数秒内即验证了式(41)成立.

对于式(41)在n不确定的情况时，直接在Maple下键入:

可将原不等式化为如下的等价形式:

注意到0≤x≤π，对式(42)两端同乘2(cos(x)－1)，然后用左端减去右端并运行Maple的simplify指令，即在Maple下键入:

可将式(42)化简为

由于0≤x≤π，sin(x)＞0且 cos(nx)＜1，因此式(43)显然成立.这样不必调用BOTTEMA，就可以完成式(41)的证明.

例15［27］最近，文献［27］考虑了这样的一个积分不等式，已知g(s)在区间［0，1］上是可积分的，对于积分不等式:

是否对一切在区间［0，1］上是可积的g(s)，上面的积分不等式均成立?

该不等式可等价地化为如下的多项式不等式［27］:

式中:xi≥0，n≥1.

计算机耗时不足1 s即能证明式(44)成立.

另外，文献［23］还讨论了如下的不等式:

该不等式可等价地化为如下的不等式［23］:

这是一个较难证明的不等式，尝试用BOTTEMA尚未成功.文献［23］分析不等式(45)时指出其难点在于π的超越性，但又声称此难点可通过将π看成一个参数，并加约束条件3＜π＜4来克服.对此我们持质疑态度，因为容易验证，将π代之以3和4时，对于确定的n，例如，当n分别为 2，3，4，…时，不等式(45)并不是总成立的！给出不等式(45)令人信服的机器证明方法，仍是一个值得深入研究的问题.

最后，文献［32］在总结各种不等式证明方法时，也给出了一批例子，这些例子大多数是属于Tarski模型的不等式类型，对此类不等式来讲，BOTTEMA的算法是完备的，当然可以直接用BOTTEMA指令给出其证明.文献［32］中还有个别含有任意多个变元的非Tarski模型不等式，大都可以通过前一节中的常用不等式加以证明，当然也可用BOTTEMA给出其机器证明.为完整起见，将证明这些例子的BOTTEMA指令在附录B中给出，此处不再展开详细的讨论和说明.

3结论

本文借助不等式证明软件BOTTEMA，给出了几类常用的基本不等式的机器证明方法，这些不等式包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等，这些不等式通常含有的变元个数可以是任意多个，属于Tarski模型外的不等式类型，充分体现了机器证明的优点，另外通过大量例子表明了问题的广泛性及软件算法的有效性.

几点注记如下.

1)BOTTEMA是一个高效能的程序，通过反复试验能够证明和发现许多过去靠计算机难以证明的不等式.结合人工证明和巧妙的代换方法，可充分发挥BOTTEMA的效能.

2)机器证明方法直接、实用、简单，所得结论有可能推广已知的不等式，其方法本身对同类不等式是有示范性的.对同一问题，机器证明技巧本身也可以有多种尝试方法，并且，机器证明的指令往往较为简洁.

3)由于算法的完备性，BOTTEMA所得条件均是充分必要的.这是一般数值算法所无法比拟的.BOTTEMA在不等式不成立时可以自动输出反例.

4)BOTTEMA使用部分柱形代数分解，忽略了边界情况的考虑，因此具有较高的效能.但对细化边界情况的讨论是有意义的研究课题.

5)BOTTEMA处理带有根式的不等式，由于降维方法的引入，尤为有效.BOTTEMA是一个不断更新的软件，不断会有新方法的引入(例如差分代换方法等).

7)BOTTEMA的实际功能要强大得多，例如，BOTTEMA的全局优化功能就有待进一步开发，这里用以对于非Tarski模型的机器证明，只调用了其最基本的功能，通过上面的例子，已显示其强大的威力.BOTTEMA作为一个强有力的工具，新的创新性的应用值得深入探索，可以预见其广泛的应用前景，应当引起控制工程界足够的重视.

8)复杂度问题是符号计算的固有瓶颈，在问题参数较多、维数较高的情况下，复杂度增长较快，如何提高效率，使之方便地应用于大规模工程优化问题，是长期值得探讨的研究课题.数值与符号运算的结合以及大规模并行运算处理，可能是提高其效率的有效途径.

附录A BOTTEMA简易使用指南［1］

上世纪90年代，本文第一作者杨路及其团队利用多项式的判别序列［6，14］、吴方法［3－5］及部分的柱形代数分解算法［7－11］，给出了能自动发现不等式的实用算法.这些算法对一大类不等式型定理是完备的，并在 Maple 下编制了通用程序 BOTTEMA［15－19］，特别地，BOTTEMA也实现了杨路提出的降维算法，能够有效处理含参根式，并能最大限度地缩减维数.BOTTEMA已成功验证了包含上百个公开问题在内的上千个代数与几何不等式，在Pentium IV 2.2 GB的CPU上证明Bottema等人专著中的100个基本几何不等式［22］，总共所用的 CPU 时间仅2 s多［1］.

BOTTEMA是用Maple实现的一个证明器，其证明不等式的过程完全自动化，其间无需人工干预.它作为一个高效的通用证明器，实现了作者多个原创的算法，包含多个实用程序.本文第一作者杨路编写了BOTTEMA的最初版本，夏时洪博士曾对程序的优化和完善承担了主要任务.BOTTEMA的源文件可从“中国不等式研究网站(http://www.irgoc.org)”下载，也可与本文作者联系获取.

下面给出本文涉及的所用指令的BOTTEMA简易使用指南，详细内容可参考文献［1］.需要说明的是，由于这是一个简易的使用指南，以下介绍的只是软件的主要功能，并不包括所有的函数.

A.1 如何安装和运行BOTTEMA

BOTTEMA是在Maple平台上开发的应用程序，如果离开了Maple您将无法使用这个程序.因此首先将BOTTEMA拷贝到您的计算机的某个子目录之下，譬如说:X:YYZZ.在进入Maple环境后您就可以运行这个程序了.

首先读入BOTTEMA(或者BOTTEMA.dat，如果该程序带扩展名的话)，即键入:

＞read“X:/YY/ZZZ/BOTTEMA”;或者

＞ read“X:/YY/ZZZ/BOTTEMA.dat”;

注意标点“、”是不能省略的，然后您就可以执行BOTTEMA的所有指令，使用其所有功能.

A.2 关于三角形中几何不变量的约定记号列表(可扩充)

如果您需要证明某个三角形中的几何不等式，那么在输入指令时对其中一些主要的几何不变量必须采用约定的记号，如下所列.

a、b、c:三角形各边之长.

s=(a+b+c)/2:三角形周长之半.

x=s－a，y=s－b，z=s－c.

R:外接圆半径.

r:内切圆半径.

ra、rb、rc:各旁切圆半径.

ha、hb、hc:各边对应的高.

ma、mb、mc:各边对应的中线长.

wa、wb、wc:各边对应的内角平分线长

S:三角形的面积.

p=4*r*(R－2*r).

q=s2－16*R*r+5*r2.

A、B、C:三角形的各内角.

sin(A):角的正弦，其他三角函数类似.

abs():绝对值.

aa:这是一个约束条件，表示讨论的是一个锐角三角形.

这些代表几何不变量的记号在BOTTEMA中属于保留字符，对它们赋值是无效的.代数不等式没有约定记号和保留字符(除Maple固有的保留字符之外).

A.3 证明不等式型定理的主要指令及其例解

A.3.1 prove

目的:证明某个三角形中的几何不等式或与之等价的代数不等式.

输入指令:prove(ineq);或 prove(ineq，［ineqs］);

指令中各项的含义如下.

ineq:一个待证的不等式，它是用上面列表中的几何不变量来表述的.

ineqs:作为假设条件的一组不等式，其每一个都是用上面列出的几何不变量来表述的.

需要注意的是:

1)待证的几何不等式必须是“＜=”型或者“＞=”型，而且作为假设条件的那组不等式定义一个开集或者一个开集加上它的全部或部份边界;ineq和ineqs必须由上述列出的几何不变量的有理函数或根式表示.

2)指令prove也适用于这样的命题:其假设ineqs和结论ineq都是用x、y、z(x＞0，y＞0，z＞0)的有理函数或根式表示的齐次代数不等式，它是“＜=”型或者“＞=”型，而且作为假设条件的那组不等式定义一个开集或者一个开集加上它的全部或部份边界.这样的代数命题等价于一个几何不等式命题.

例子:

A.3.2 xprove

目的:证明某个具有非负变量的代数不等式.

输入指令:xprove(ineq);或 xprove(ineq，［ineqs］);

指令中各项的含义如下.

ineq:一个待证的代数不等式，它的所有变量都取非负值.

ineqs:作为假设条件的一组代数不等式，其中所有变量都取非负值.

需要注意的是:

1)待证的代数不等式必须是“＜=”型或者“＞=”型，而且作为假设条件的不等式组ineqs定义一个开集或者一个开集加上它的全部或部份边界(由于后一限制，当原问题的假设条件中含有某个等式P=Q时，必须用消元的方法去掉等式并降低整个问题的维数，绝不能简单地用2个不等式P＞=Q，P＜=Q代替).

2)其假设ineqs和结论ineq中只出现有理函数和根式.

3)“所有变量非负”在此是默认的，不必写入假设条件中.

例子:

A.3.3 yprove

目的:证明某个代数不等式.

输入指令:yprove(ineq);或 yprove(ineq，［ineqs］);

指令中各项的含义如下.

ineq:一个待证的代数不等式.

ineqs:作为假设条件的一组代数不等式.

需要注意的是:

1)待证的代数不等式必须“＜=”型或者“＞=”型，而且作为假设条件的不等式组ineqs定义一个开集或者一个开集加上它的全部或部份边界(由于后一限制，当原问题的假设条件中含有某个等式P=Q时，必须用消元的方法去掉等式并降低整个问题的维数，绝不能简单地用2个不等式P＞=Q，P＜=Q代替).

2)其假设ineqs和结论ineq中只出现有理函数和根式.

例子:

A.3.4 sprove

目的:证明某个具有非负变量的对称的多项式不等式.

输入指令:sprove(ineq);

ineq:一个待证的具有非负变量的对称的多项式不等式.

“非负变量”在此是默认的.

目前BOTTEMA尚未考虑另加约束条件的sprove.

A.4 关于全局优化的主要指令及其例解(略)

由于本文并未涉及BOTTEMA的全局优化指令，因此这里省略了BOTTEMA关于全局优化的主要函数功能及其指令例解的介绍，感兴趣的读者可参见文献［1］.

附录B 文献［37］中例子的 BOTTEMA机器证明指令

上述所有指令耗用的计算机CPU时间均在秒级范围之内.

［1］杨路，夏壁灿.不等式机器证明与自动发现:数学机械化丛书［M］.北京:科学出版社，2008.

［2］TARSKI A.A decision method for elementary algebra and geometry［M］.Berkeley，USA:The University of California Press，1951.

［3］吴文俊.初等几何判定问题与机械化证明［J］.中国科学:数学，1977，20(6):507－516.

WU Wenjun.On the decision problem and mechanization of theorem－proving in elementary－geometry［J］.Science China Mathemation，1977，20(6):507－516.

［4］吴文俊.几何定理机器证明的基本原理［M］.北京:科学出版社，1984.

［5］吴文俊.数学机械化:数学机械化丛书［M］.北京:科学出版社，2003.

［6］杨路，张景中，侯晓荣.非线性代数方程组与机器证明:非线性科学丛书［M］.上海:上海科学教育出版社，1996.

［7］ARNON D S，COLLINS G E，MCCALLUM S.Cylindrical algebraic decomposition I:the basic algorithm［J］.SIAM Journal on Computing，1984，13(4):865－877.

［8］ARNON D S，COLLINS G E，MCCALLUM S.Cylindrical algebraic decomposition II:an adjacency algorithm for the plane［J］.SIAM Journal on Computing，1984，13(4):878－889.

［9］BROWN C W.Simple CAD construction and its applications［J］.Journal of Symbolic Computation，2001，31(5):521－547.

［10］COLLINS G E.Quantifier elimination for real closed fields by cylindrical algebraic decomposition［C］//Automata Theory and Formal Languages.Kaiserslautern，Germany，1975:134－183.

［11］COLLINS G E，HONG H.Partial cylindrical algebraic decomposition for quantifier elimination［J］.Journal of Symbolic Computation，1991，12(3):299－328.

［12］CHOU S C.Mechanical geometry theorem proving［M］.Dordrecht， Holland:D.Reidel Publishing Company，1988.

［13］CHOU S C，ZHANG J Z，GAO X S.Machine proofs in geometry:automated production of readable proofs for geometry theorems［M］.Singapore:World Scientific，1994.

［14］杨路，侯晓荣，曾振柄.多项式的完全判别系统［J］.中国科学:E 辑，1996，26(5):424－441.

YANG Lu，HOU Xiaorong，ZENG Zhenbing.A complete discrimination system for polynomials［J］.Science in China:Series E，1996，26(5):424－441.

［15］杨路.不等式机器证明的降维算法与通用程序［J］.高技术通讯，1998，8(7):20－25.

YANG Lu.A dimension－decreasing algorithm with generic program for automated inequalities proving［J］.High Technology Letters，1998，8(7):20－25.

［16］YANG Lu.Practical automated reasoning on inequalities:generic programs for inequality proving and discovering［C］//Proceedings of the Third Asian Technology Conference in Mathematics.Tsukuba，Japan，1998:24－35.

［17］YANG Lu.Recent advances in automated theorem proving on inequalities［J］.Journal of Computer Science and Technology，1999，14(5):434－446.

［18］杨路，夏时洪.一类构造性几何不等式的机器证明［J］.计算机学报，2003，26(7):769－778.

YANG Lu，XIA Shihong.Automated proving for a class of constructive geometric inequalities［J］.Chinese Journal of Computer，2003，26(7):769－778.

［19］YANG Lu，ZHANG Ju.A practical program of automated proving for a class of geometric inequalities［C］//The Third International Workshop on Automated Deduction in Geometry.London，UK:Springer－Verlag，2001:41－57.

［20］杨路，侯晓荣，夏壁灿.自动发现不等式型定理的一个完备算法［J］.中国科学:E辑，2001，31(3):424－441.

YANG Lu，HOU Xiaorong，XIA Bican.A complete algorithm for automated discovering of a class of inequality－type theorems［J］.Science in China:Series E，2001，31(3):424－441.

［21］DOLZMANN A，STURM T.REDLOG:computer algebra meets computer logic［J］.ACM SIGSAM Bulletin，1997，31(2):2－9.

［22］BOTTEMA O，DORDEVIC R Z，JANIC R R，et al.Geometric inequlities［M］.Groningen，The Netherlands:Wolters－Noordhoff Publishing，1969.

［23］GERHOLD S，KAUERS M.A procedure for proving special function inequalities involving a discrete parameter［C］//Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation.New York，USA:ACM Press，2005:156－162.

［24］GERHOLD S，KAUERS M.A computer proof of Turán inequality［J］.Journal of Inequalities in Pure and Applied Mathematics，2006，7(2):Article 42.

［25］KAUERS M.Computer proofs for polynomials identities in arbitrary many variables［C］//Proceedings of the 2004 International Smposium on Symbolic and Agebraic Cmputation.New York，USA:ACM Press，2004:199－204.

［26］杨路，姚勇，冯勇.Tarski模型外的一类机器可判定问题［J］.中国科学:A 辑，2007，37(5):513－522.

YANG Lu，YAO Yong，FENG Yong.A class of machine determination problem besides the Tarski model［J］.Science China:Series A，2007，37(5):513－522.

［27］YANG Lu，YU Wensheng，YUAN Ruyi.Mechanical decision for a class of intergral inequalities［J］.Science China Information Sciences，2010，53(9):1800－1815.

［28］HARDY G H，LITTLEWOOD J E，POLYA G.Inequalities［M］.Cambridge，UK:Cambridge University Press，1988.

［29］MARSHALL A W，OLKIN I.Inequalities:theory of majorization and its applications［M］.New York，USA:Academic Press，1979.

［30］MITRINOVIC D S.Elementary inequlities［M］.Groningon，The Netherlands:P.Noordhoff Ltd.，1964.

［31］MITRINOVIC D S，VASIC P M.Analytic inequalities［M］.Berlin，Germany:Springer，1970.

［32］张福春，李姿霖.不等式之基本解题方法［J］.数学传播，2007，31(2):38－61.

ZHANG Fuchun，LI Zilin.The basic problem－solving methods for inequality［J］.Mathematical Communication，2007，31(2):38－61.

［33］匡继昌.常用不等式［M］.4版.济南:山东科学技术出版社，2010.

［34］ACZEL J.Some general methods in the theory of functional equations in one variable:new applications of functional equations［J］.Uspekhi Matematicheskikh Nauk，1956，11(3):3－68.

［35］ACZEL J，VARGA O.Bemerkung zur Cayley－Kleinschen Massbestimmung［J］.Punl Math，1955，4:3－15.

［36］NANJUNDIAH T S.Problem 10347［J］.The American Mathematical Monthly，1993，100(10):951－952.

［37］BEESACK P R.On certain discrete inequalities involving partial sums［J］.Canadian Journal of Mathematics，1969，21:222－234.

杨路，男，1936年生，教授，博士生导师，主要研究方向为定理机器证明、数学机械化与推理自动化、计算代数几何特别是计算实代数几何及其在信息技术领域的应用等.

郁文生，男，1967年生，教授，博士生导师，博士，主要研究方向为鲁棒控制、泛函微分方程理论、符号计算和实代数理论及应用、系统全局优化、数学机械化与推理自动化及其在信息技术领域的应用等.

Automated proving of some fundamental applied inequalities

YANG Lu，YU Wensheng
(Shanghai Key Laboratory of Trustworthy Computing，East China Normal University，Shanghai 200062，China)

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－geometricharmonic 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.

fundamental applied inequalities;automated proving;inequality－proving package BOTTEMA;Tarski model

TP181

A

1673－4785(2011)05－0377－14

10.3969/j.issn.1673－4785.2011.05.001

2011－04－13.

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

郁文生.E－mail:wsyu@sei.ecnu.edu.cn.