第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=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 =(n+1)*(t+x*y）, 序和大于等于乱序和”的证明. [r*s>=n*t,n*x≥T,n*y=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)A0,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)'=(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
·382. 智能系统学报 第6卷 m≤n时的情形，此时式(22)在r=1,即n=m时成 xprove((r+x2)0,m≥1n≥mM-1=0]); 这里为明确起见，给出凸函数与凹函数的定义 同样可在不到1s的时间内证明式(22)成立，因为 如下. 可以令C=∑4D=∑4c=4 定义2函数f称为在区间ICR上的凸函数， 最后，对于Bernoulli不等式(21)或(22)在r取 若满足a1,a2∈1,0=(t+(x+y)2), [r+s+s*sqt(r*s)>=]); D=4a)E=a 屏幕显示“The inequalitity holds”,于是式(24)右边 则显然有A≤(1-t+1)B+t+1C(凸性定义)及B≤ 的不等式即可得证，因为可以令r、、t、xy分别代表 D(归纳假设).注意到0<t1<2<…<k+1<1, ∑E=1ak、∑t=ib2、∑t=1(ak+be)2、a+1、bn+1,而式 ∑1：=1及 (24)在n=1时显然成立. （1-tk1)D+k+C=E, 对于式(24)左边的不等式，可以对c=a+b和 于是，自然有 d=-b应用式(24)右边的不等式即可，也可以类似 A≤(1-te+1)D+t+1C=E. 于式(24)右边不等式的机器证明，执行BOTTEMA 上式当然也可通过执行BOTTEMA的yprove指令： 的xprove指令： yprove(A <(1-t)*D+t*C,[A <
第5期 杨路，等：常用基本不等式的机器证明 ·383· (1-t)*B+t*C,B0,1-t>0]); 不等式 从而得证 例3[1，用机器证明Turn不等式： 2更多的实例 △n(x):=Pn(x)2-Pn-1(x)P+1(x)>0, x∈[-1,1]，n≥1. 本节提供更多的具有典型意义的不等式机器证 式中：P.(x)表示第n个Legendre多项式. 明的例子，包括文献[23-24]中所有例子的B0TTE 首先，因为P(x)=1,P1(x)=x,P2(（x）= MA机器证明实现.为完整起见，列出文献[1]中已 (3x2-1)/2,所以容易验证不等式在n=1时成立. 经用BOTTEMA机器证明实现的几个典型例子.需 其次，考虑归纳步骤： 要说明的是，对于文献[23-24]中的例子，当时作者 △.(x)≥0→△+1(x)≥0， 是借助QEPCADU以及Mathematica平台下的CAD x∈[-1,1]，n≥1. (28) 包给出其机器证明的，并特别指出这些例子以前从 如果把P。-1、Pn、P+1、P+2分别命名为Y1、Y、Y、 未被机器自动证明过，但可以看到，这些例子基于 Y2,则式(28)变成量词消去问题： BOTTEMA机器证明实现时，可能更为方便简洁. (Y1,Yo,Y,Y2)-Y1Y1≥0= 例112a]证明文献[30]中的一个不等式： Y-YY2≥0. (29) 式(29)显然为假，于是需要添加一些条件，根据 Wn+W(n-1)+W…+√2+≤ Legendre多项式的递归性质： Wm+1,n≥1. (n+2)Pn+2(x)=(2n+3)xP1(x)- 显然n=1时上式成立.记上式左端为r,归纳 (n+1)Pn(x),n≥0. 步骤变成证明 那么，修改后的量词消去问题变为： (Hn≥1，r>0)r≤Wn+1→ H(N,X,Y1,Y,Y,Y2)(N≥0，-1≤X≤1， √n+1+T≤√n+1+1. (N+2)Y2=(2N+3)XY,-(N+1)Y, 使用BOTTEMA的prove指令： (N+1)Y1=(2N+1)XY-NY-1, xprove(sqrt(n +1 +r)1]); 这个命题的假设条件中包括2个等式，必须通过降维 可在几秒内证明上式成立. (消元)去掉等号后才能应用BOTTEMA程序.根据这 例2】证明 2个等式消去变量Y,、Y2之后，得到一个仅含有4个 a-∑a-∑p)≤ 变量X、Y,、Y-1、N的新命题.该命题可以用yprove指 令在几秒钟内证明成立，即完成了归纳证明。 (1-w)2 例4a】证明 对一切满足下列条件的实数x:yk成立 (30) ≤1,2≤1. 则2出>0.2 显然n=2时式(30)成立.将式(30)左端中的 这个所要证明的不等式称为Aczl不等式，可 以看作是Cauchy不等式的双曲版本，在非欧几何中 正因子a!去掉，并记Σ：为，使用B0 有应用，它首先是由Acz等提出并证明的3435， TEMA的xprove指令： 显然只要证明该不等式对于一切正数xkyk成 xprove(r+a >0,[r 0]); 立就够了，所以仍用BOTTEMA的xprove指令来完 及 成如下归纳步骤： xprove(r +a-b >0, （Hr,s,,x,y)1-8-x2≥0,1-t-y2≥0， [r>0,r+a>0,b<a]); (1-s)(1-t)≤(1-r)2→ 计算机耗时不足18即证明式(30)成立.这里之所 (1-8-x2)(1-t-y2)≤(1-r-xy)2 以用2条prove指令，是因为分别考虑了当n为奇 执行指令： 数或偶数时的递推。 pove(1-s-x2)*(1-t-y2)≤(1-r-y)2, 例51证明文献[30]中3.27的-个不等式： [1-s-x2≥0,1-t-y2≥0， (31) (1-s)*(1-t)≤(1-r)2]): <G)2<n,n≥2. BOTTEMA在验证了1156个样本点后证明了Aczl 式中：Cg是寻常的二项系数，即
.384· 智能系统学报 第6卷 cg=a(a-1)a-2)(a-(a-102 yprove((x Y2 +Y)21/(4*(n+1), 3 1 3一3≤R-2≤2十， [A>1/(4*n),n>=2]); n≥3，x∈R. (34) 为证式(31)右端的不等式，使用B0 TTEMA的 显然式(34)在n=3成立.分别执行BOTTEMA prove指令： 的xprove指令： xprove((2*n+2)2*(2*n+1)2* prove((1+n/R-1/2)2=(n-3/4),(R-1/2)2=2]); (n+1/4),n>=1,R>=1]); 计算机耗时不足1s即能证明式(31)成立， 例62a1证明文献[31]中3.2.12所谓的Lein 及 xprove(1+n/R-1/2)2>=(n+1-3/4), 不等式： 1sI+n [(R-1/2)2>=(n-3/4),(R-1/2)2=1,R>=1]); 0=(n+2)*r*x, [n*r*x+1>=(n+1)*r]); 显然式(35)在n=1时成立.记A=∑=1√斥， 为证式(32)右端的不等式，执行BOTTEMA的 B=∑：=，执行BOTTEMA的kprove指令： xprove指令： xprove((A+(n+1)n)2=1]); (n+1)*(2+n)*(1-x)2/2, 计算机在2s内证明式(35)成立. [n*r*x+1=(B a-b)2, (33) [A+a2>=(B+a)2,a>=b]); 式中：R表示实数集合 及 显然式(33)在n=3和n=4时成立.记Y,= xprove(A-a2+62>=(B-a+b)2, F.（x),Y2=F.+1,A=(x2+2)-3,使用B0 TTEMA [A-a2>=(B-a)2,A>B2,a>=b]); 的yprove指令： 计算机耗时不足1：即能证明式(36)成立.这里之
第5期 杨路，等：常用基本不等式的机器证明 ·385· 所以用2条xprove指令，是因为分别考虑了当n为 xprove((1 +A+a)C*(1-a), 2引>2 [1/(1+A)>C]); 品 21* n-1' xprove(1 -A-a C*(1-a), [(1-A)>C,a n-1 (37) 计算机耗时不足1s即能证明式(38)和(39)成立. 之=1 例132】考虑文献[37]中的不等式（文献 式中：xk>0,x2>4x1,n≥2. [23]在给出式(40)时有一个明显的打印错误，将式 显然式(37)在n=2时成立.记 (40)左端x的一个下标k误印为i了)： A=了2-’6三=2下， k 三（月P≤（店）9n≥1.（40) 式中：xk>0,a≥1且a+B≥1.该不等式对于确定的 C=∑，D=∑，E= n+一 a和B是可以机器证明的.下面给出α=2，B=-1 ∑ 情形的证明. 对于式(37)中的第1个不等式，执行B0 TTEMA的 显然式(40)在n=1时成立.记A=∑=，B= xprove指令： ∑t=1（∑1x)-x,执行BOTTEMA的xprove指令： xprove(A C/D (n +1)2/n, xprove(B+/(A+x)n2/(n-1),n>=2,C>=D]); 计算机耗时不足1s即能证明式(40)成立 对于式(37)中的第2个不等式，执行B0 TTEMA的 例142】考虑文献[30]中5.16的不等式： xprove指令： xprove(B +E (n +1)/n, Ain()≥2in(aw）, [B>n/(n-1),n>=2]); 0≤x≤T,n≥1. (41) 计算机耗时不足1s即能证明式(37)成立.事实上， 式(41)在n确定时就是普通的三角不等式，文 式(37)中的第2个不等式不用机器证明，可直接由 献[30]中验证了n=1,2,3,4的情形.在处理三角 下面显然成立的不等式得到. 不等式时，BOTTEMA具有极高的效率，例如，即使 1>"a≥2 n 取n=90,依然可以执行BOTTEMA的prove指令： 例1223】证明文献[31]中3.2.37所谓的 prove(subs(n =90,sum(sin(*A), k=1.n)>sin(n*A)/2); Weierstrass不等式： 计算机在数秒内即验证了式(41)成立. 对于式(41)在n不确定的情况时，直接在Ma ple下键入： (38) sum(sin(x),k =1..n)sin(nx)/2; 及 可将原不等式化为如下的等价形式： >1-a）>1-a 1+a sin(n)sinc((1) 2 co8(x)-1 (39) 2in(a+10）-号o25a里2+2m(e). 式中：n≥1,0B*(1+a), (sin(x)*cos((n+1)*x)-8in((n+1)*x)* [1/(1-A)>B,A+a<1]); (cos(x)-1)-sin(x)cos(x)sin(x)*
.386. 智能系统学报 第6卷 (cos(x)-1)); 给出其机器证明.为完整起见，将证明这些例子的 可将式(42)化简为 BOTTEMA指令在附录B中给出，此处不再展开详 sin(x)(cos(nx)-1)0且cos(nx)=0, 是有示范性的.对同一问题，机器证明技巧本身也可 [n7*B-A8>=0,n>=1]); 以有多种尝试方法，并且，机器证明的指令往往较为 计算机耗时不足18即能证明式(44)成立， 简洁. 另外，文献[23]还讨论了如下的不等式： 3)由于算法的完备性，BOTTEMA所得条件均 店忌 ,nCgn≥1. 是充分必要的.这是一般数值算法所无法比拟的. BOTTEMA在不等式不成立时可以自动输出反例. 该不等式可等价地化为如下的不等式3)： 4)BOTTEMA使用部分柱形代数分解，忽略了 若-1-4+1G< 3k2+3k+1 边界情况的考虑，因此具有较高的效能.但对细化边 界情况的讨论是有意义的研究课题. nCg,n≥1. 2 (45) 5)BOTTEMA处理带有根式的不等式，由于降 维方法的引入，尤为有效.BOTTEMA是一个不断更 这是一个较难证明的不等式，尝试用BOTTEMA尚 新的软件，不断会有新方法的引人（例如差分代换 未成功.文献[23]分析不等式(45)时指出其难点在 方法等). 于π的超越性，但又声称此难点可通过将π看成一 6)BOTTEMA目前尚不适合处理类似sinx< 个参数，并加约束条件3<π<4来克服.对此我们 持质疑态度，因为容易验证，将T代之以3和4时， <m(0<x<受)这样的超越不等式，这是值得 对于确定的n,例如，当n分别为2,3,4，…时，不等 进一步研究的课题， 式(45)并不是总成立的！给出不等式(45)令人信 7)BOTTEMA的实际功能要强大得多，例如， 服的机器证明方法，仍是一个值得深人研究的问题 BOTTEMA的全局优化功能就有待进一步开发，这 最后，文献[32]在总结各种不等式证明方法 里用以对于非Tarski模型的机器证明，只调用了其 时，也给出了一批例子，这些例子大多数是属于Tar 最基本的功能，通过上面的例子，已显示其强大的威 ski模型的不等式类型，对此类不等式来讲，B0TTE 力.BOTTEMA作为一个强有力的工具，新的创新性 MA的算法是完备的，当然可以直接用BOTTEMA指 的应用值得深入探索，可以预见其广泛的应用前景， 令给出其证明.文献[32]中还有个别含有任意多个 应当引起控制工程界足够的重视。 变元的非Tarski模型不等式，大都可以通过前一节 8)复杂度问题是符号计算的固有瓶颈，在问题 中的常用不等式加以证明，当然也可用BOTTEMA 参数较多、维数较高的情况下，复杂度增长较快，如