第5期 杨路，等：常用基本不等式的机器证明 ·383· (1-t)*B+t*C,B<=D,t>0,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)<=sqrt(n +1)+1, %-YY1≥0)→-YY2≥0. [r<=sqt(n)+1,n>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是寻常的二项系数，即