.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不等式的机器证明