第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 算机上实际判定一些难度不大的代数与几何的非平
·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个
第5期 杨路，等：常用基本不等式的机器证明 ·379· 正实数，则 对于算术与几何平均不等式(1)的机器证明， a“T. 还可以采取多种其他不同的策略，例如，容易知道， n n 日 算术与几何平均不等式(1)等价于如下的Jacobsthal 不等式[]： 显然，仅需对n个正实数a1,a2,…,an,证明如 (Ha>0,b>0,n≥1)(n-1)a"+b"≥ 下的算术与几何平均不等式： na"-1b. (8) “Ta, (1) 事实上，只需在式(5)中令￥=片，即可得到式(5) 与式(8)的等价性.式(8)对于n=1的情形是显然 即可直接证明几何与调和平均不等式，因为1,1 a1'a2 成立的，用数学归纳法完成式(8)的证明，只需引进 …,1皆为正实数，利用式(1)有 新变元s、t,执行BOTTEMA的xprove指令： an xprove(n*s*a+tb>= (n+1)*s*a*b,[(n-1)*s*a+t>=n*s*b]); ≥ (2) 屏幕几乎立即提示“The inequalitity holds'”. n 对于几何与调和平均不等式(3)，也可仿照上 将式(2)取倒数即得 述过程给出其机器证明方法，当然，直接利用算术与 VΠ4≥ n (3) 几何平均不等式(1)证明几何与调和平均不等式 (3)的过程也是非常简单的 如果考虑如下的算术与调和平均不等式： 下面给出式(1)的证明.容易验证式(1)在n= 1时成立.按照数学归纳法，假设式(1)成立，则需要 ≥n ∑”1 (9) 证明 n N+I 2k=1 dx T 类似上面的讨论，引进新变元A、B,执行BOTTEMA 的prove指令： 亦成立.由于式(1)成立，只需证 xprove((A +a)/(n +1)>= n3VT4+a≥(n+1)Va 4中 (n+1)/(B+1/a),[A/n>n/B]); 上式可以改写成： 即完成了式(9)的机器证明. I +1 l.2 Cauchy不等式的机器证明 n· a +1≥(n+1) (4) Cauchy不等式(Cauchy inequality）设x1,2, …,xn及y1,y2,…,y为2组实数数列，则 方便起见，作代换 正=心，式4)变为 +1 （∑)2≤∑∑元 an+l nx+1+1≥(n+1)x”. 该不等式的机器证明实现参见文献[1,23]，文献 (5) [23]基于QEPCAD,而文献[1]是基于BOTTEMA 现在，仅需证明式(5)对任意正数x和任意正整数n 成立即可.仍用数学归纳法，记式(5)为中，显然1 的.下面采用文献[1]的方法，记中n是如下公式： 成立.为证 (∑tw)-∑a∑ti≤0， 中n→中n+1, (6) 容易验证中1和中2成立.按照数学归纳法，需要证明 这时引进新的变元「，考虑命题： 中→0n+1: (10) (Vr>0,x>0,n≥1)nrx+1≥(n+1)r→ 这时引进新的变元r、s、t、xy,考虑命题： (n+1)rx2+1≥(n+2)rx. (7) （HT,s,t,x,y）r2≤st→ 如果式(7)为真，那么式(6)当然就为真，因为可以 (r+y)2≤(s+x2)(t+y2). (11) 令T代表x”,由于r、x、n全都是非负，因此可以执行 如果式(11)为真，那么式(10)当然就为真，因为可 BOTTEMA的xprove指令： 以令T、s、t、xy分别代表∑t=xy、∑t=1x、∑=1yi、 xprove((n +1)**1>= x+1y+…但式(11)和式(10)显然并不等价，事实 (n+2)*r*x,[n*T*x+1>=(n+1)*r]); 上，如果对实变量T、s、、x、y不附加任何其他条件的 屏幕几乎立即提示“The inequalitity holds”.这即完 话，命题式(11)是不成立的. 成了算术几何平均不等式的证明. 注意，式(11)是一个实量词消去问题，因而
.380. 智能系统学报 第6卷 它是否为真是可以判定的.譬如，可以执行B0TTE 等于乱序和”来证明“乱序和大于等于逆序和”，这 MA的yprove指令： 只需对2组实数a1≤a2≤…≤an及-bn≤-bn-1≤ yprove((r+x*y)2<=(s+x2)*(t+y2), …≤一b1应用“顺序和大于等于乱序和”即可.这样 [2<=s*t]); 即完成了排序不等式的证明. 屏幕几乎立即提示“The inequalitity does not hold”, 1.4 Chebyshev不等式的机器证明 即该命题一般不为真 Chebyshev不等式(Chebyshev inequality)设 不过显而易见，如果已经证明Cauchy不等式对 a1≤a2≤…≤an及b1≤b2≤…≤bn为两递增实数 于所有的x≥0，y≥0成立，那么当xy。为一般实 列，则 数时它也必然成立.这样不妨假设x、ys非负，从而 r、s、t全都是非负的.于是可以执行BOTTEMA的 ∑ia6t≤h（∑ia)(∑tb)≤ xprove指令： ∑iaa4e xprove((r+x*y)2<=(s+x2)*(t+y2), [r2<=s*t]); Chebyshev不等式当然可以由排序不等式证得， 下面给出基于BOTTEMA的证明方法，为使机器证 经大约0.05s之后屏幕提示“The inequalitity holds”,这即完成了Cauchy不等式的证明， 明更好地体现Chebyshev不等式前提中的单调性条 件，引进比“单调数列”更广泛的所谓“均和单调数 1.3排序不等式的机器证明 排序不等式(arrangement inequality）设有2组实 列”的概念 数有序数列a,≤a2≤…≤an及b1≤b2≤…≤bn,则 定义1给定数列{a,i=1,2,…,若满足条件： ∑ib≥ (顺序和) 4 ≤am+1,n=1,2,…, ∑a6≥ (乱序和) 则称该数列是均和不城的：若上式中的不等号反向 ∑.a6l+ (逆序和) 成立，则称该数列是均和不增的；若不等式严格成 式中：ji2,…jn是1,2，…，n的任一排序。 立，则称该数列是均和递增（递减）的. 排序不等式可以导出许多不等式，例如算术与 显然，单调递增的数列是均和不减的，单调递减 几何平均不等式、Cauchy不等式及下一小节的Che 的数列是均和不增的， 先证 byshev不等式等. 先证明“顺序和大于等于乱序和”，令S= （%)(i4)≤∑iao.(uB) ∑=ab,不妨假设S中j.≠n(若j,=n则考虑 注意到“均和单调数列”的定义，只需执行BOTTE jn-1),则在S中存在某个m≠n,使得bn与am搭 MA的yprove指令： 配，即在S中含有项anmb.(m≠n),因此，只要 yprove((r+x)*(s +y)<=(n+1)*(t+x*y), ambn+abn≥anb.+abn (12) [r*s<=n*t,n*x>=T,n*y>=s,n>=1]); 成立，即表明当jn≠n时，调换S中bn和b.的位置 仅需数秒，屏幕显示“The inequalitity holds”,于是式 (其余n-2项保持不变)，会使S增加.同理可证其 (13)即可得证，因为可以令T、s、t、x、y分别代表 他ak必须和bk搭配(k=1,2,…,n-1). ∑t=1ak、∑t=1bk、∑=1axbk、an+1、bn+1,而式(13)在 为证式(12)，只需执行BOTTEMA的yprove指令： n=1时显然成立. yprove((am bi an*b>= 为证 am *bn +an *bi), [am <=an,bi<=b]); ∑iab4≤1（∑a4)(∑b), 即可得证.事实上，式(12)亦容易从下式中直接得 (14) 到323 注意到∑t=1b:=∑k=!bn+1-k,可以对{bn}进行重新 (am-an)(bn-bn)≥0. 排序，将其视为均和不增的，类似于式(13)的证明， 这里调用BOTTEMA的yprove指令，只是为了 只需执行BOTTEMA的yprove指令： 说明本文机器证明方法的统一性，这即完成了“顺 powe(r+x)*(s+y）>=(n+1)*(t+x*y）, 序和大于等于乱序和”的证明. [r*s>=n*t,n*x≥T,n*y<=s,n>=1]): 仿照上述过程可以给出“乱序和大于等于逆序 式(14)即可得证. 和”的机器证明，当然，也可直接利用“顺序和大于 这样即完成了Chebyshev不等式的机器证明
第5期 杨路，等：常用基本不等式的机器证明 ·381· 事实上，这就已经证明Chebyshev不等式对于均和 可在不到1s的时间内证明式(21)成立 单调的数列都是成立的，这已经在一定程度上推广 2)对于Bernoul山i不等式(21)中r取负整数的 了原来的Chebyshev不等式类型. 情形，此时式(21)在r=0时成立.记x=a+1,A= 对于上面通过BOTTEMA指令yprove证明的2 x“,归纳步骤变成证明 个命题，还有另一种较简单的，甚至可认为是机器明 (HA>0,x>0,n≥1)A≥1-n(x-1)→ 证(certificate)的方法，也是富有启发性的，在同 Ax1≥1-(n+1)*(x-1)). 类问题的机器证明中可能会有效.这里也简单介绍 使用BOTTEMA的xprove指令： 它的证明过程如下， prove(A/x>=1-(n+1)*(x-1), 命题1若s≤nt,nx≥r,y≥s,n≥1，则 [A>=1-n*(x-1)]); (r+x)(s+y）≤(n+1)(t+xy).(15) 同样可在不到18的时间内证明式(21)成立. 证明根据题设，不妨令 3)对于Bemoulli不等式(22)中r取1的情形， t=开+0，x=7+p,y=+q,(16) 此时式(22)在r=1时成立.记x=a+1,A=x,归 式中：0≥0，P≥0,9≥0，将式(16)代入 纳步骤变成证明 (n+1)(t+y）-(r+x)(s+y), 化简整理得 (A>0,>0,n>1)A<1+x-1)= wn pnq w. (17) 式(17)显然是非负的，于是式(15)成立，命题1得证 A<1+a*(-1). 类似地，可以证明如下的命题， 使用BOTTEMA的prove指令： 命题2若s≥nt,nx≥r,y≤s,n≥1，则 xprove(A<1+(1/(n+1))*(x*A-1), (r+x)(s+y)≥(n+1)(t+y).(18) [A<1+(1/n)*(x-1)]); 证明根据题设，不妨令 同样可在不到1s的时间内证明式(22)成立 =-=+py= -9,(19) ,m≥n时的 4)对于Bernoulli不等式(21)中r=m, n 式中：0≥0，p≥0,9≥0，将式(19)代人 情形，此时式(21)在r=1,即m=n时成立.固定n对m (r+x)(s+y)-(n+1)(t+xy), 应用归纳法，记x=a+1,A=x°，归纳步骤变成证明 化简整理，得 (VA>0,n≥1，m≥n)4≥1+%(A-1)→ wn png w. (20) 式(20)显然是非负的，于是式(18)成立，命题2得证 A1≥1+m+1*(A°-1)， n 命题1和命题2的证明根本无需B0 TTEMA,在 亦即 任何符号计算软件平台上都容易验证， 1.5 Bernoulli不等式的机器证明 (HA>0,n≥1，m≥n)A-1≥m(A"-1)→ Bernoulli不等式(Bernoulli inequality)】 设 41-1≥m+1*(A-1). a>-1,且r≥1或r≤0，则 n (1+a)'≥1+ar; (21) 而 若r的范围为(0,1)，则有 A-1=(A-10∑4 (1+a)'<1+ar (22) 于是，使用BOTTEMA的xprove指令： 成立 xprove(A-1)*(D+d)>=(A-1)*C*(m+1)/n, 1)Bernoull山i不等式(21)针对r取正整数情形的 [(A-1)*D>=(A-1)*C*m/n,m>=n, 机器证明实现参见文献[1].事实上，式(21)在r=1 (d-D/m)*(A-1)>=0]); 时成立.记x=a+1,A=x”,归纳步骤变成证明 即可在不足1s的时间内证明式(21)成立，因为可以令 (HA>0,x>0,n≥1)A≥1+n(x-1)→ C=t=4-D=∑A-1、d=Am.该条指令中的(d- A*x≥1+（n+1)*(x-1). D/m)*(A-1)>=0体现了数列{A,k=1,2,…}的单 使用BOTTEMA的xprove指令： 调性（或更准确地说，均和单调性）. xprove(A*x>=1+(n+1)*（x-1), [A>=1+n*(x-1)]): 5)类似地，对于Bernoulli不等式(22)中r= n