·382. 智能系统学报 第6卷 m≤n时的情形，此时式(22)在r=1,即n=m时成 xprove((r+x2)<=(t+(x-y)2+2* 立.固定m对n应用归纳法，记x=a+1,A=x·,归 8qrt((t+(x-y)2)*(s+y2))+(s+y2), 纳步骤变成证明 [r<=t+2*sqt(t*s)+s]); 即可得证.这样就完成了三角形不等式的机器证明. (VA>0,m≥1n≥mM-1<g-1= 1.7 Jensen不等式的机器证明 4”-1<n年1*(4m-1). Jensen不等式(Jensen inequality)设函数f在 区间ICR上为一凸函数，a1,a2,…,an∈I且0< 使用BOTTEMA的prove指令： t1<t2<…<tn<1,t1=1,则 xprove((A-1)*D<(A-1)(C +c)* r∑taa)≤tha). (25) m/(n+1),[(A-1)*D<(A-1)*C*m/n 若f为一凹函数，则将式(25)的不等式变号。 m<=n,(c-C/n)*(A-1)>=0]); 这里为明确起见，给出凸函数与凹函数的定义 同样可在不到1s的时间内证明式(22)成立，因为 如下. 可以令C=∑4D=∑4c=4 定义2函数f称为在区间ICR上的凸函数， 最后，对于Bernoulli不等式(21)或(22)在r取 若满足a1,a2∈1,0<A<1,且 任意实数的情形，可由有理数在实数中的稠密性和 f(Aa1+(1-入)a2)≤ 指数函数的连续性，再结合上面的诸结论得到，这样 fa)+(1-A)f(a2). (26) 即完成了Bernoulli不等式的机器证明. 若将式(26)的不等式变号，则f即为凹函数 1.6三角形不等式的机器证明 最常见的Jensen不等式是，若f为凸函数且t1= 三角形不等式(triangle inequality)设a= 2=…=6,=1,则 (a1,a2,…,an)和b=(b1,b2,…,bn)为2个向量，则 n Ia1-Ib1≤Ia+bI≤IaI+lb1.(23) 从几何角度看，式(23)右边不等式即三角形中 ≤ (27) n 任意两边长的和大于第三边长，式(23)左边不等式 同理，若∫为凹函数，则将式(27)的不等式变号. 即三角形中任意两边长的差小于第三边长， Jensen不等式当然可用数学归纳法直接得 三角不等式当然可以由Cauchy不等式证得.下 证2].下面给出迂回的代换方法，本质上与文献 面给出基于BOTTEMA的证明方法，根据向量模的 [32]的方法相同，只是为了说明在机器证明不等式 定义，即是要证明 的过程中，如何处理像Jensen不等式这样含有未具 √∑t-√t.院≤√∑(a:+b)2≤ 体给出明确定义的函数f的情形，这也是为了说明 机器证明方法的统一性. √∑匠+√∑经 (24) 利用数学归纳法.由定义2知Jensen不等式在 先证式(24)右边的不等式，易见，此时不等式 n=2时成立.若假设Jensen不等式在n=k时成立， 若对所有的ae≥0，bk≥0成立，那么当ak、bk为一般 考察n=k+1的情形，作如下代换： 实数时它也必然成立.这样只需执行BOTTEMA的 A=f∑a,), xprove指令： xprove((++2*sqrt((r+2)* B=a小.c=a (s+y2))+(s+y2)>=(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 <