.384· 智能系统学报 第6卷 cg=a(a-1)a-2)(a-(a-102 yprove((x Y2 +Y)2<= 1×2×3×…×a (x2+1)2*A*(x2+2)2,[<=(x2+1)2*A, a(a-1)(a-2)…(a-(a-1), 经<=(x2+1)2*A*(x2+2)]); 计算机在2s内即能证明式(33)成立， 并约定C。=1. 例8】证明文献[36]中的定义的如下递推 显然式(31)在m=2时成立记6cC,)户为4， 公式： 为证式(31)左端的不等式，使用BOTTEMA的 R1=1+尺，n≥1，R=1, prove指令： 则 xprove((2*n+2)2*(2*n+1)2* (A/16)/(n+1)4>1/(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+1+1/4), A/16/(n+1)4<(1/(3*(n+1)+1), [(R-1/2)2>=(n-3/4),(R-1/2)2<= [A<1/(3*n+1),n>=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<= a+)2≤1+(1-x (n+1/4),n>=1,R>=1]); 0<x≤1，n≥0. (32) 计算机耗时不足1s能证明式(34)成立. 式(32)左端的不等式已在证明算术几何平均 例9[21 证明文献[30]中4.15的一个相关不 不等式的过程中完成，只需执行BOTTEMA的 等式： xprove指令： （宫A≤（n≥1. (35) prove(n+1)*r*x2+1>=(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<=(B+(n+1)3)3, xprove(n+1)*r*x2+1<=(n+2)*r*x+ [A2<B3,n>=1]); (n+1)*(2+n)*(1-x)2/2, 计算机在2s内证明式(35)成立. [n*r*x+1<=(n+1)*r+ 例102】证明文献[31]中第112页Thm.6的 n*(1+n)*(1-x)2/2,x<=1]): 一个不等式： 计算机耗时不足1s即证明式(32)成立. 例71证明文献[31]中3.3.38的递推不等 含-金≥（宫-1a只(6） 式，若记Fn(x)为第n个Fibonacci多项式，其递推 式中：(a)k1是正的递减的序列， 定义如下： 显然式(36)在n=1时成立.记 Fn+2(x)=xF+1+F.(x),F(x)=1,F2(x)=x, A= ∑ta(-1)d,B=∑（-10k'a, 则 使用BOTTEMA的xprove指令： F2≤(x2+1)2(x2+2)-3,n≥3，x∈R, xprove(A a2-b2>=(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)成立.这里之