楊路，郁文生

(華東師范大學(xué)上海高可信計算重點(diǎn)實驗室，上海 200062)

常用基本不等式的機(jī)器證明

楊路，郁文生

(華東師范大學(xué)上海高可信計算重點(diǎn)實驗室，上海 200062)

不等式機(jī)器證明問題是智能系統(tǒng)領(lǐng)域的難點(diǎn)和熱點(diǎn)問題.借助不等式證明軟件BOTTEMA，對若干常用的基本不等式成功地實現(xiàn)了機(jī)器證明，包括算術(shù)、幾何與調(diào)和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所論不等式含有的變元個數(shù)是一個不確定的變量，屬于Tarski模型外的不等式類型.機(jī)器證明得出的結(jié)論有時可能是已知結(jié)果的推廣，其方法本身對同類不等式有示范性，更多的例子表明了該算法和軟件的有效性.

基本不等式;機(jī)器證明;不等式證明軟件BOTTEMA;Tarski模型

不等式的機(jī)器證明問題，一直是數(shù)學(xué)機(jī)械化、自動推理及智能系統(tǒng)領(lǐng)域的研究難點(diǎn)和熱點(diǎn)問題，近年來取得了長足的進(jìn)展，已有專著《不等式機(jī)器證明與自動發(fā)現(xiàn)》［1］問世.早在20世紀(jì)50年代初，波蘭數(shù)學(xué)家Tarski［2］發(fā)表了著名的論文《初等代數(shù)與初等幾何的判定方法》，證明了初等代數(shù)以及初等幾何范圍的命題可以用機(jī)械的步驟來判定其正確與否，此種問題被稱為機(jī)器(或算法)可判定的，也稱為Tarski模型內(nèi)的問題，該模型的任何一個確定的公式中變元的個數(shù)都是確定的有限數(shù).但另一方面由著名的G¨odel不完全性定理可知，機(jī)器可判定的問題類在數(shù)學(xué)中相對較少，即使在看似最簡單的初等數(shù)論這一范圍，其中命題的機(jī)器判定從整體而言也是不可能實現(xiàn)的.

對于Tarski模型內(nèi)的問題，Tarski最早的判定算法僅在理論上解決問題，由于其計算復(fù)雜度太高，實際上不可能判定任何非平凡的代數(shù)和幾何命題［1，3－6］.后來，經(jīng) Collins 提出又經(jīng)他人合作改進(jìn)的“柱形代數(shù)剖分(cylindrical algebraic decomposition，CAD)”算法［7－11］，效率上有很大提高，已經(jīng)能夠在計算機(jī)上實際判定一些難度不大的代數(shù)與幾何的非平凡命題，但作為定理機(jī)器證明的一個通用程序，計算復(fù)雜度仍然很高.

1977年吳文?。?］提出的初等幾何定理機(jī)器判定的新方法(吳方法)是這一領(lǐng)域的重大突破［4－6］.吳方法(Wu method)主要是針對等式型命題的判定方法.吳方法的成功在世界范圍內(nèi)推動了機(jī)器證明代數(shù)方法研究的加速發(fā)展［1，4－6，12－13］，但對不等式機(jī)器證明的研究仍是舉步維艱，不等式機(jī)器證明的困難在于它依賴于實代數(shù)的自動推理.1996年楊路等［6，14］建立的多項式完全判別系統(tǒng)(a complete discrimination system for polynomials，CDS)為實代數(shù)自動推理提供了有效的工具，使得不等式機(jī)器證明的成果得以普遍接受并付諸實際應(yīng)用.

自20 世紀(jì) 90 年代以來，楊路及其團(tuán)隊［15－20］利用多項式的判別序列［6，14］、吳方法［3－5］和部分的柱形代數(shù)分解算法［7－11］，給出了能自動發(fā)現(xiàn)不等式的實用算法，這些算法對一大類不等式型定理是完備的，并在 Maple 下編制了通用程序 BOTTEMA［15－19］和Discoverer［20］.基于柱形代數(shù)分解方法的著名軟件還有 REDLOG［21］和 QEPCAD［11］以及 Mathematica 平臺下的CAD包等.這些軟件包都具有很強(qiáng)的實用性，例如，通用程序BOTTEMA已成功驗證了包含上百個公開問題的上千個代數(shù)與幾何不等式，在Pentium IV 2.2 GB的CPU上證明Bottema等人專著中的100個基本幾何不等式［22］，總共所用的CPU時間僅2 s多［1］，但上述各軟件所處理的問題類基本屬于Tarski模型.

信息與科學(xué)技術(shù)及數(shù)學(xué)某些領(lǐng)域問題中出現(xiàn)的不等式有時可能會依賴于一個(甚至多個)離散參數(shù)n，它是一個不確定的自然數(shù)，譬如一些用傳統(tǒng)數(shù)學(xué)歸納法證明的命題，這類問題已經(jīng)超出了Tarski的判定算法所能處理的“初等范圍”，但是這類問題并不等于不能轉(zhuǎn)化為Tarski的判定算法所能處理的“初等類型”.事實上，已經(jīng)有學(xué)者借助 QEPCAD［11］以及Mathematica平臺下的CAD包，用計算機(jī)模擬數(shù)學(xué)歸納法［23－25］，文獻(xiàn)［1］中也用 BOTTEMA 證明了許多以前未考慮過能用機(jī)器證明的不等式，這是對某些非Tarski模型命題類進(jìn)行機(jī)械化證明的有啟發(fā)性的嘗試.最近，文獻(xiàn)［26－27］分別給出了實用的算法，用于判定一類變元個數(shù)是變量的多項式正性和一類積分不等式命題，并在Maple平臺上，根據(jù)該算法設(shè)計完成了程序，可以快速實現(xiàn)判定目標(biāo)，這也屬于Tarski模型外的機(jī)器可判定問題.研究討論Tarski模型以外具有實際應(yīng)用價值的機(jī)器可判定問題類是極具重要科學(xué)意義和發(fā)展前景的研究課題.

當(dāng)今，不等式的重要應(yīng)用已貫穿于當(dāng)代科學(xué)技術(shù)與工程領(lǐng)域的多個學(xué)科分支［1］.不等式的理論很早就被大數(shù)學(xué)家高斯(Gauss)、柯西(Cauchy)等人著重研究，而哈代(Hardy)、李特爾伍德(Littlewood)和波利亞(Pólya)［28］、Marshall和 Olkin［29］及 Mitrinovi［30－31］等著名數(shù)學(xué)家也相繼投入探討.可以說數(shù)學(xué)分析，不論是純理論還是應(yīng)用，都需要不等式的運(yùn)算［32］.

2007年，張福春和李姿霖發(fā)表了題為《不等式之基本解題方法》的論文［32］，系統(tǒng)總結(jié)了幾類常用基本不等式的證明及其應(yīng)用，這些不等式包括算術(shù)、幾何與調(diào)和平均不等式、Cauchy不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.這些不等式均依賴于離散參數(shù)n，它是一個不確定的自然數(shù)，明顯屬于Tarski模型外的不等式類型.

本文結(jié)合不等式證明軟件BOTTEMA，給出幾類常用的基本不等式的機(jī)器證明方法.這些不等式包含了文獻(xiàn)［32］中的幾類基本不等式，其中，對Cauchy不等式的機(jī)器證明實現(xiàn)參見文獻(xiàn)［1，23］，Bernoulli不等式針對正整數(shù)情形的機(jī)器證明實現(xiàn)參見文獻(xiàn)［1］.另外，也給出文獻(xiàn)［23－24］中所有例子的BOTTEMA機(jī)器證明實現(xiàn).這些不等式含有的變元個數(shù)均是任意多個，都屬于Tarski模型外的不等式類型.最后通過大量的例子來表明問題的廣泛性及軟件算法的有效性.

應(yīng)該指出，文獻(xiàn)［32］及本文中出現(xiàn)的不等式，均是經(jīng)典的著名不等式，已有大量的相關(guān)研究，個別不等式已有幾十種甚至上百種巧妙的人工證明方法［33］.本文的新意和貢獻(xiàn)在于結(jié)合不等式證明軟件BOTTEMA，給出這些常用基本不等式的機(jī)器證明方法，體現(xiàn)機(jī)器證明的優(yōu)點(diǎn).機(jī)器證明方法得出的結(jié)論有可能推廣已知的不等式，其方法本身對同類不等式是有示范性的.當(dāng)然，針對具體的不等式，可以采用多種不同的機(jī)器證明策略，本文盡可能應(yīng)用較為直接的策略.

1 常用基本不等式的機(jī)器證明

本節(jié)給出幾類常用基本不等式基于不等式證明軟件BOTTEMA的機(jī)器證明過程.BOTTEMA的簡易使用指南［1］可見附錄A.

用BOTTEMA證明不等式，常常僅需輸入1條(或多條)相應(yīng)的BOTTEMA指令即可，為便于理解，針對幾類常用基本不等式，在給出相應(yīng)BOTTEMA指令的同時，也給出采用機(jī)器證明策略的詳細(xì)分析過程.

1.1 算術(shù)、幾何與調(diào)和平均不等式的機(jī)器證明

算術(shù)、幾何與調(diào)和平均不等式(arithmetic－geometric－h(huán)armonic inequality) 設(shè) a1，a2，…，an為 n 個正實數(shù)，則

顯然，僅需對n個正實數(shù)a1，a2，…，an，證明如下的算術(shù)與幾何平均不等式:

將式(2)取倒數(shù)即得

下面給出式(1)的證明.容易驗證式(1)在n=1時成立.按照數(shù)學(xué)歸納法，假設(shè)式(1)成立，則需要證明

亦成立.由于式(1)成立，只需證

上式可以改寫成:

現(xiàn)在，僅需證明式(5)對任意正數(shù)x和任意正整數(shù)n成立即可.仍用數(shù)學(xué)歸納法，記式(5)為φn，顯然φ1成立.為證

這時引進(jìn)新的變元r，考慮命題:

如果式(7)為真，那么式(6)當(dāng)然就為真，因為可以令r代表xn.由于r、x、n全都是非負(fù)，因此可以執(zhí)行BOTTEMA的xprove指令:

(n+2)*r*x，［n*r*x+1＞=(n+1)*r］);屏幕幾乎立即提示“The inequalitity holds”.這即完成了算術(shù)幾何平均不等式的證明.

對于算術(shù)與幾何平均不等式(1)的機(jī)器證明，還可以采取多種其他不同的策略，例如，容易知道，算術(shù)與幾何平均不等式(1)等價于如下的Jacobsthal不等式［33］:

(n+1)*s*a*b，［(n－1)*s*a+t＞=n*s*b］);屏幕幾乎立即提示“The inequalitity holds”.

對于幾何與調(diào)和平均不等式(3)，也可仿照上述過程給出其機(jī)器證明方法，當(dāng)然，直接利用算術(shù)與幾何平均不等式(1)證明幾何與調(diào)和平均不等式(3)的過程也是非常簡單的.

如果考慮如下的算術(shù)與調(diào)和平均不等式:

類似上面的討論，引進(jìn)新變元A、B，執(zhí)行BOTTEMA的xprove指令:

即完成了式(9)的機(jī)器證明.

1.2 Cauchy不等式的機(jī)器證明

Cauchy不等式(Cauchy inequality) 設(shè)x1，x2，…，xn及y1，y2，…，yn為 2 組實數(shù)數(shù)列，則

該不等式的機(jī)器證明實現(xiàn)參見文獻(xiàn)［1，23］，文獻(xiàn)［23］基于 QEPCAD［11］，而文獻(xiàn)［1］是基于 BOTTEMA的.下面采用文獻(xiàn)［1］的方法，記φn是如下公式:

容易驗證φ1和φ2成立.按照數(shù)學(xué)歸納法，需要證明

這時引進(jìn)新的變元r、s、t、x、y，考慮命題:

注意，式(11)是一個實量詞消去問題［11］，因而它是否為真是可以判定的.譬如，可以執(zhí)行BOTTEMA的yprove指令:

屏幕幾乎立即提示“The inequalitity does not hold”，即該命題一般不為真.

不過顯而易見，如果已經(jīng)證明Cauchy不等式對于所有的xk≥0，yk≥0 成立，那么當(dāng)xk、yk為一般實數(shù)時它也必然成立.這樣不妨假設(shè)xk、yk非負(fù)，從而r、s、t全都是非負(fù)的.于是可以執(zhí)行 BOTTEMA的xprove指令:

經(jīng)大約 0.05 s之后屏幕提示“The inequalitity holds”，這即完成了Cauchy不等式的證明.

1.3 排序不等式的機(jī)器證明

排序不等式(arrangement inequality) 設(shè)有2組實數(shù)有序數(shù)列a1≤a2≤…≤an及b1≤b2≤…≤bn，則

式中:j1，j2，…，jn是 1，2，…，n的任一排序.

排序不等式可以導(dǎo)出許多不等式，例如算術(shù)與幾何平均不等式、Cauchy不等式及下一小節(jié)的Chebyshev不等式等.

先證明“順序和大于等于亂序和”.令S=akbjk，不妨假設(shè)S中jn≠n(若jn=n則考慮jn－1)，則在S中存在某個m≠n，使得bn與am搭配，即在S中含有項ambn(m≠n).因此，只要

成立，即表明當(dāng)jn≠n時，調(diào)換S中bn和bjn的位置(其余n－2項保持不變)，會使S增加.同理可證其他ak必須和bk搭配(k=1，2，…，n－1).

為證式(12)，只需執(zhí)行BOTTEMA的yprove指令:

即可得證.事實上，式(12)亦容易從下式中直接得到［32－33］.

這里調(diào)用BOTTEMA的yprove指令，只是為了說明本文機(jī)器證明方法的統(tǒng)一性.這即完成了“順序和大于等于亂序和”的證明.

仿照上述過程可以給出“亂序和大于等于逆序和”的機(jī)器證明，當(dāng)然，也可直接利用“順序和大于等于亂序和”來證明“亂序和大于等于逆序和”，這只需對2組實數(shù)a1≤a2≤…≤an及 －bn≤ －bn－1≤…≤－b1應(yīng)用“順序和大于等于亂序和”即可.這樣即完成了排序不等式的證明.

1.4 Chebyshev不等式的機(jī)器證明

Chebyshev不等式(Chebyshev inequality) 設(shè)a1≤a2≤…≤an及b1≤b2≤…≤bn為兩遞增實數(shù)列，則

Chebyshev不等式當(dāng)然可以由排序不等式證得，下面給出基于BOTTEMA的證明方法.為使機(jī)器證明更好地體現(xiàn)Chebyshev不等式前提中的單調(diào)性條件，引進(jìn)比“單調(diào)數(shù)列”更廣泛的所謂“均和單調(diào)數(shù)列”的概念.

定義1 給定數(shù)列{ai，i=1，2，…}，若滿足條件:

則稱該數(shù)列是均和不減的;若上式中的不等號反向成立，則稱該數(shù)列是均和不增的;若不等式嚴(yán)格成立，則稱該數(shù)列是均和遞增(遞減)的.

顯然，單調(diào)遞增的數(shù)列是均和不減的，單調(diào)遞減的數(shù)列是均和不增的.

先證

注意到“均和單調(diào)數(shù)列”的定義，只需執(zhí)行BOTTEMA的yprove指令:

為證

式(14)即可得證.

這樣即完成了Chebyshev不等式的機(jī)器證明.事實上，這就已經(jīng)證明Chebyshev不等式對于均和單調(diào)的數(shù)列都是成立的，這已經(jīng)在一定程度上推廣了原來的Chebyshev不等式類型.

對于上面通過BOTTEMA指令yprove證明的2個命題，還有另一種較簡單的，甚至可認(rèn)為是機(jī)器明證(certificate)［1］的方法，也是富有啟發(fā)性的，在同類問題的機(jī)器證明中可能會有效.這里也簡單介紹它的證明過程如下.

命題 1若rs≤nt，nx≥r，ny≥s，n≥1，則

證明根據(jù)題設(shè)，不妨令

式中:w≥0，p≥0，q≥0，將式(16)代入

化簡整理得

式(17)顯然是非負(fù)的，于是式(15)成立，命題1得證.

類似地，可以證明如下的命題.

命題 2若rs≥nt，nx≥r，ny≤s，n≥1，則

證明根據(jù)題設(shè)，不妨令

式中:w≥0，p≥0，q≥0，將式(19)代入

化簡整理，得

式(20)顯然是非負(fù)的，于是式(18)成立，命題2得證.

命題1和命題2的證明根本無需BOTTEMA，在任何符號計算軟件平臺上都容易驗證.

1.5 Bernoulli不等式的機(jī)器證明

Bernoulli不等式(Bernoulli inequality) 設(shè)a＞ －1，且r≥1 或r≤0，則

若r的范圍為(0，1)，則有

成立.

1)Bernoulli不等式(21)針對r取正整數(shù)情形的機(jī)器證明實現(xiàn)參見文獻(xiàn)［1］.事實上，式(21)在r=1時成立.記x=a+1，A=xn，歸納步驟變成證明

使用BOTTEMA的xprove指令:可在不到1 s的時間內(nèi)證明式(21)成立.

2)對于Bernoulli不等式(21)中r取負(fù)整數(shù)的情形，此時式(21)在r=0時成立.記x=a+1，A=x－n，歸納步驟變成證明

使用BOTTEMA的xprove指令:

同樣可在不到1 s的時間內(nèi)證明式(21)成立.

使用BOTTEMA的xprove指令:

同樣可在不到1 s的時間內(nèi)證明式(22)成立.

于是，使用BOTTEMA的xprove指令:

使用BOTTEMA的xprove指令:

最后，對于Bernoulli不等式(21)或(22)在r取任意實數(shù)的情形，可由有理數(shù)在實數(shù)中的稠密性和指數(shù)函數(shù)的連續(xù)性，再結(jié)合上面的諸結(jié)論得到，這樣即完成了Bernoulli不等式的機(jī)器證明.

1.6 三角形不等式的機(jī)器證明

三角形不等式(triangle inequality) 設(shè)a=(a1，a2，…，an)和 b=(b1，b2，…，bn)為 2 個向量，則

從幾何角度看，式(23)右邊不等式即三角形中任意兩邊長的和大于第三邊長，式(23)左邊不等式即三角形中任意兩邊長的差小于第三邊長.

三角不等式當(dāng)然可以由Cauchy不等式證得.下面給出基于BOTTEMA的證明方法，根據(jù)向量模的定義，即是要證明

先證式(24)右邊的不等式，易見，此時不等式若對所有的ak≥0，bk≥0成立，那么當(dāng)ak、bk為一般實數(shù)時它也必然成立.這樣只需執(zhí)行BOTTEMA的xprove指令:

對于式(24)左邊的不等式，可以對c=a+b和d=－b應(yīng)用式(24)右邊的不等式即可，也可以類似于式(24)右邊不等式的機(jī)器證明，執(zhí)行BOTTEMA的xprove指令:

即可得證.這樣就完成了三角形不等式的機(jī)器證明.

1.7 Jensen不等式的機(jī)器證明

Jensen不等式(Jensen inequality) 設(shè)函數(shù)f在區(qū)間I?R 上為一凸函數(shù)，a1，a2，…，an∈I且 0 ＜t1＜t2＜…＜tn＜1，=1，則

若f為一凹函數(shù)，則將式(25)的不等式變號.

這里為明確起見，給出凸函數(shù)與凹函數(shù)的定義如下.

定義2函數(shù)f稱為在區(qū)間I?R上的凸函數(shù)，若滿足a1，a2∈I，0 ＜ λ ＜1，且

若將式(26)的不等式變號，則f即為凹函數(shù).

同理，若f為凹函數(shù)，則將式(27)的不等式變號.

Jensen不等式當(dāng)然可用數(shù)學(xué)歸納法直接得證［32］.下面給出迂回的代換方法，本質(zhì)上與文獻(xiàn)［32］的方法相同，只是為了說明在機(jī)器證明不等式的過程中，如何處理像Jensen不等式這樣含有未具體給出明確定義的函數(shù)f的情形，這也是為了說明機(jī)器證明方法的統(tǒng)一性.

利用數(shù)學(xué)歸納法.由定義2知Jensen不等式在n=2時成立.若假設(shè)Jensen不等式在n=k時成立，考察n=k+1的情形，作如下代換:

于是，自然有

上式當(dāng)然也可通過執(zhí)行BOTTEMA的yprove指令:

(1－t)*B+t*C，B＜=D，t＞0，1－t＞0］);從而得證.

2 更多的實例

本節(jié)提供更多的具有典型意義的不等式機(jī)器證明的例子，包括文獻(xiàn)［23－24］中所有例子的BOTTEMA機(jī)器證明實現(xiàn).為完整起見，列出文獻(xiàn)［1］中已經(jīng)用BOTTEMA機(jī)器證明實現(xiàn)的幾個典型例子.需要說明的是，對于文獻(xiàn)［23－24］中的例子，當(dāng)時作者是借助QEPCAD［11］以及Mathematica平臺下的CAD包給出其機(jī)器證明的，并特別指出這些例子以前從未被機(jī)器自動證明過，但可以看到，這些例子基于BOTTEMA機(jī)器證明實現(xiàn)時，可能更為方便簡潔.

例 1［1，23］證明文獻(xiàn)［30］中的一個不等式:

顯然n=1時上式成立.記上式左端為r，歸納步驟變成證明

使用BOTTEMA的xprove指令:

可在幾秒內(nèi)證明上式成立.

例 2［1］證明

對一切滿足下列條件的實數(shù)xk、yk成立.

這個所要證明的不等式稱為Aczél不等式，可以看作是Cauchy不等式的雙曲版本，在非歐幾何中有應(yīng)用，它首先是由 Aczél等提出并證明的［34－35］.

顯然只要證明該不等式對于一切正數(shù)xk、yk成立就夠了，所以仍用BOTTEMA的xprove指令來完成如下歸納步驟:

執(zhí)行指令:

BOTTEMA在驗證了1 156個樣本點(diǎn)后證明了Aczél不等式.

例 3［1，24］用機(jī)器證明 Turán 不等式:

式中:Pn(x)表示第n個Legendre多項式.

首先，因為P0(x)=1，P1(x)=x，P2(x)=(3x2－1)/2，所以容易驗證不等式在n=1時成立.其次，考慮歸納步驟:

如果把Pn－1、Pn、Pn+1、Pn+2分別命名為Y－1、Y0、Y1、Y2，則式(28)變成量詞消去問題:

式(29)顯然為假，于是需要添加一些條件.根據(jù)Legendre多項式的遞歸性質(zhì):

那么，修改后的量詞消去問題變?yōu)?

這個命題的假設(shè)條件中包括2個等式，必須通過降維(消元)去掉等號后才能應(yīng)用BOTTEMA程序.根據(jù)這2個等式消去變量Y1、Y2之后，得到一個僅含有4個變量X、Y0、Y－1、N的新命題.該命題可以用 yprove 指令在幾秒鐘內(nèi)證明成立，即完成了歸納證明.

例 4［23］證明

計算機(jī)耗時不足1 s即證明式(30)成立.這里之所以用2條xprove指令，是因為分別考慮了當(dāng)n為奇數(shù)或偶數(shù)時的遞推.

例5［23］證明文獻(xiàn)［30］中3.27的一個不等式:

式中:是尋常的二項系數(shù)，即

為證式(31)右端的不等式，使用 BOTTEMA的xprove指令:

計算機(jī)耗時不足1 s即能證明式(31)成立.

例6［23］證明文獻(xiàn)［31］中3.2.12所謂的Levin不等式:

式(32)左端的不等式已在證明算術(shù)幾何平均不等式的過程中完成，只需執(zhí)行 BOTTEMA的xprove指令:

為證式(32)右端的不等式，執(zhí)行 BOTTEMA的xprove指令:

計算機(jī)耗時不足1s即證明式(32)成立.

例7［23］證明文獻(xiàn)［31］中3.3.38的遞推不等式，若記Fn(x)為第n個Fibonacci多項式，其遞推定義如下:

式中:R表示實數(shù)集合.

顯然式(33)在n=3和n=4時成立.記Y1=Fn(x)，Y2=Fn+1，A=(x2+2)n－3，使用 BOTTEMA的yprove指令:

計算機(jī)在2 s內(nèi)即能證明式(33)成立.

例8［23］證明文獻(xiàn)［36］中的定義的如下遞推公式:

顯然式(34)在n=3成立.分別執(zhí)行BOTTEMA的xprove指令:

計算機(jī)耗時不足1 s能證明式(34)成立.

例9［23］證明文獻(xiàn)［30］中4.15的一個相關(guān)不等式:

顯然式(35)在n=1時成立.記A=，執(zhí)行BOTTEMA的xprove指令:

計算機(jī)在2 s內(nèi)證明式(35)成立.

例10［23］證明文獻(xiàn)［31］中第112頁Thm.6的一個不等式:

式中:(ak)k≥1是正的遞減的序列.

顯然式(36)在n=1時成立.記

使用BOTTEMA的xprove指令:

［A－a2＞=(B－a)2，A＞B2，a＞=b］);計算機(jī)耗時不足1 s即能證明式(36)成立.這里之所以用2條xprove指令，是因為分別考慮了當(dāng)n為奇數(shù)或偶數(shù)時的遞推.

例11［23］證明文獻(xiàn)［30］中7.31與7.32出現(xiàn)的相關(guān)不等式:

式中:xk＞0，x2＞4x1，n≥2.

顯然式(37)在n=2時成立.記

對于式(37)中的第1個不等式，執(zhí)行BOTTEMA的xprove指令:

對于式(37)中的第2個不等式，執(zhí)行BOTTEMA的xprove指令:

計算機(jī)耗時不足1 s即能證明式(37)成立.事實上，式(37)中的第2個不等式不用機(jī)器證明，可直接由下面顯然成立的不等式得到.

例12［23］證明文獻(xiàn)［31］中 3.2.37所謂的Weierstrass不等式:

式中:n≥1，0＜a＜1且＜1.

k

顯然式(38)和式(39)在n=1時成立.記

依次執(zhí)行如下BOTTEMA的xprove指令:

計算機(jī)耗時不足1 s即能證明式(38)和(39)成立.

例13［23］考慮文獻(xiàn)［37］中的不等式(文獻(xiàn)［23］在給出式(40)時有一個明顯的打印錯誤，將式(40)左端x的一個下標(biāo)k誤印為i了):

式中:xk＞0，α≥1且α+β≥1.該不等式對于確定的α和β是可以機(jī)器證明的.下面給出α=2，β=－1情形的證明.

例14［23］考慮文獻(xiàn)［30］中5.16的不等式:

式(41)在n確定時就是普通的三角不等式，文獻(xiàn)［30］中驗證了n=1，2，3，4 的情形.在處理三角不等式時，BOTTEMA具有極高的效率，例如，即使取n=90，依然可以執(zhí)行BOTTEMA的prove指令:

計算機(jī)在數(shù)秒內(nèi)即驗證了式(41)成立.

對于式(41)在n不確定的情況時，直接在Maple下鍵入:

可將原不等式化為如下的等價形式:

注意到0≤x≤π，對式(42)兩端同乘2(cos(x)－1)，然后用左端減去右端并運(yùn)行Maple的simplify指令，即在Maple下鍵入:

可將式(42)化簡為

由于0≤x≤π，sin(x)＞0且 cos(nx)＜1，因此式(43)顯然成立.這樣不必調(diào)用BOTTEMA，就可以完成式(41)的證明.

例15［27］最近，文獻(xiàn)［27］考慮了這樣的一個積分不等式，已知g(s)在區(qū)間［0，1］上是可積分的，對于積分不等式:

是否對一切在區(qū)間［0，1］上是可積的g(s)，上面的積分不等式均成立?

該不等式可等價地化為如下的多項式不等式［27］:

式中:xi≥0，n≥1.

計算機(jī)耗時不足1 s即能證明式(44)成立.

另外，文獻(xiàn)［23］還討論了如下的不等式:

該不等式可等價地化為如下的不等式［23］:

這是一個較難證明的不等式，嘗試用BOTTEMA尚未成功.文獻(xiàn)［23］分析不等式(45)時指出其難點(diǎn)在于π的超越性，但又聲稱此難點(diǎn)可通過將π看成一個參數(shù)，并加約束條件3＜π＜4來克服.對此我們持質(zhì)疑態(tài)度，因為容易驗證，將π代之以3和4時，對于確定的n，例如，當(dāng)n分別為 2，3，4，…時，不等式(45)并不是總成立的！給出不等式(45)令人信服的機(jī)器證明方法，仍是一個值得深入研究的問題.

最后，文獻(xiàn)［32］在總結(jié)各種不等式證明方法時，也給出了一批例子，這些例子大多數(shù)是屬于Tarski模型的不等式類型，對此類不等式來講，BOTTEMA的算法是完備的，當(dāng)然可以直接用BOTTEMA指令給出其證明.文獻(xiàn)［32］中還有個別含有任意多個變元的非Tarski模型不等式，大都可以通過前一節(jié)中的常用不等式加以證明，當(dāng)然也可用BOTTEMA給出其機(jī)器證明.為完整起見，將證明這些例子的BOTTEMA指令在附錄B中給出，此處不再展開詳細(xì)的討論和說明.

3結(jié)論

本文借助不等式證明軟件BOTTEMA，給出了幾類常用的基本不等式的機(jī)器證明方法，這些不等式包括算術(shù)、幾何與調(diào)和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等，這些不等式通常含有的變元個數(shù)可以是任意多個，屬于Tarski模型外的不等式類型，充分體現(xiàn)了機(jī)器證明的優(yōu)點(diǎn)，另外通過大量例子表明了問題的廣泛性及軟件算法的有效性.

幾點(diǎn)注記如下.

1)BOTTEMA是一個高效能的程序，通過反復(fù)試驗?zāi)軌蜃C明和發(fā)現(xiàn)許多過去靠計算機(jī)難以證明的不等式.結(jié)合人工證明和巧妙的代換方法，可充分發(fā)揮BOTTEMA的效能.

2)機(jī)器證明方法直接、實用、簡單，所得結(jié)論有可能推廣已知的不等式，其方法本身對同類不等式是有示范性的.對同一問題，機(jī)器證明技巧本身也可以有多種嘗試方法，并且，機(jī)器證明的指令往往較為簡潔.

3)由于算法的完備性，BOTTEMA所得條件均是充分必要的.這是一般數(shù)值算法所無法比擬的.BOTTEMA在不等式不成立時可以自動輸出反例.

4)BOTTEMA使用部分柱形代數(shù)分解，忽略了邊界情況的考慮，因此具有較高的效能.但對細(xì)化邊界情況的討論是有意義的研究課題.

5)BOTTEMA處理帶有根式的不等式，由于降維方法的引入，尤為有效.BOTTEMA是一個不斷更新的軟件，不斷會有新方法的引入(例如差分代換方法等).

7)BOTTEMA的實際功能要強(qiáng)大得多，例如，BOTTEMA的全局優(yōu)化功能就有待進(jìn)一步開發(fā)，這里用以對于非Tarski模型的機(jī)器證明，只調(diào)用了其最基本的功能，通過上面的例子，已顯示其強(qiáng)大的威力.BOTTEMA作為一個強(qiáng)有力的工具，新的創(chuàng)新性的應(yīng)用值得深入探索，可以預(yù)見其廣泛的應(yīng)用前景，應(yīng)當(dāng)引起控制工程界足夠的重視.

8)復(fù)雜度問題是符號計算的固有瓶頸，在問題參數(shù)較多、維數(shù)較高的情況下，復(fù)雜度增長較快，如何提高效率，使之方便地應(yīng)用于大規(guī)模工程優(yōu)化問題，是長期值得探討的研究課題.數(shù)值與符號運(yùn)算的結(jié)合以及大規(guī)模并行運(yùn)算處理，可能是提高其效率的有效途徑.

附錄A BOTTEMA簡易使用指南［1］

上世紀(jì)90年代，本文第一作者楊路及其團(tuán)隊利用多項式的判別序列［6，14］、吳方法［3－5］及部分的柱形代數(shù)分解算法［7－11］，給出了能自動發(fā)現(xiàn)不等式的實用算法.這些算法對一大類不等式型定理是完備的，并在 Maple 下編制了通用程序 BOTTEMA［15－19］，特別地，BOTTEMA也實現(xiàn)了楊路提出的降維算法，能夠有效處理含參根式，并能最大限度地縮減維數(shù).BOTTEMA已成功驗證了包含上百個公開問題在內(nèi)的上千個代數(shù)與幾何不等式，在Pentium IV 2.2 GB的CPU上證明Bottema等人專著中的100個基本幾何不等式［22］，總共所用的 CPU 時間僅2 s多［1］.

BOTTEMA是用Maple實現(xiàn)的一個證明器，其證明不等式的過程完全自動化，其間無需人工干預(yù).它作為一個高效的通用證明器，實現(xiàn)了作者多個原創(chuàng)的算法，包含多個實用程序.本文第一作者楊路編寫了BOTTEMA的最初版本，夏時洪博士曾對程序的優(yōu)化和完善承擔(dān)了主要任務(wù).BOTTEMA的源文件可從“中國不等式研究網(wǎng)站(http://www.irgoc.org)”下載，也可與本文作者聯(lián)系獲取.

下面給出本文涉及的所用指令的BOTTEMA簡易使用指南，詳細(xì)內(nèi)容可參考文獻(xiàn)［1］.需要說明的是，由于這是一個簡易的使用指南，以下介紹的只是軟件的主要功能，并不包括所有的函數(shù).

A.1 如何安裝和運(yùn)行BOTTEMA

BOTTEMA是在Maple平臺上開發(fā)的應(yīng)用程序，如果離開了Maple您將無法使用這個程序.因此首先將BOTTEMA拷貝到您的計算機(jī)的某個子目錄之下，譬如說:X:YYZZ.在進(jìn)入Maple環(huán)境后您就可以運(yùn)行這個程序了.

首先讀入BOTTEMA(或者BOTTEMA.dat，如果該程序帶擴(kuò)展名的話)，即鍵入:

＞read“X:/YY/ZZZ/BOTTEMA”;或者

＞ read“X:/YY/ZZZ/BOTTEMA.dat”;

注意標(biāo)點(diǎn)“、”是不能省略的，然后您就可以執(zhí)行BOTTEMA的所有指令，使用其所有功能.

A.2 關(guān)于三角形中幾何不變量的約定記號列表(可擴(kuò)充)

如果您需要證明某個三角形中的幾何不等式，那么在輸入指令時對其中一些主要的幾何不變量必須采用約定的記號，如下所列.

a、b、c:三角形各邊之長.

s=(a+b+c)/2:三角形周長之半.

x=s－a，y=s－b，z=s－c.

R:外接圓半徑.

r:內(nèi)切圓半徑.

ra、rb、rc:各旁切圓半徑.

ha、hb、hc:各邊對應(yīng)的高.

ma、mb、mc:各邊對應(yīng)的中線長.

wa、wb、wc:各邊對應(yīng)的內(nèi)角平分線長

S:三角形的面積.

p=4*r*(R－2*r).

q=s2－16*R*r+5*r2.

A、B、C:三角形的各內(nèi)角.

sin(A):角的正弦，其他三角函數(shù)類似.

abs():絕對值.

aa:這是一個約束條件，表示討論的是一個銳角三角形.

這些代表幾何不變量的記號在BOTTEMA中屬于保留字符，對它們賦值是無效的.代數(shù)不等式?jīng)]有約定記號和保留字符(除Maple固有的保留字符之外).

A.3 證明不等式型定理的主要指令及其例解

A.3.1 prove

目的:證明某個三角形中的幾何不等式或與之等價的代數(shù)不等式.

輸入指令:prove(ineq);或 prove(ineq，［ineqs］);

指令中各項的含義如下.

ineq:一個待證的不等式，它是用上面列表中的幾何不變量來表述的.

ineqs:作為假設(shè)條件的一組不等式，其每一個都是用上面列出的幾何不變量來表述的.

需要注意的是:

1)待證的幾何不等式必須是“＜=”型或者“＞=”型，而且作為假設(shè)條件的那組不等式定義一個開集或者一個開集加上它的全部或部份邊界;ineq和ineqs必須由上述列出的幾何不變量的有理函數(shù)或根式表示.

2)指令prove也適用于這樣的命題:其假設(shè)ineqs和結(jié)論ineq都是用x、y、z(x＞0，y＞0，z＞0)的有理函數(shù)或根式表示的齊次代數(shù)不等式，它是“＜=”型或者“＞=”型，而且作為假設(shè)條件的那組不等式定義一個開集或者一個開集加上它的全部或部份邊界.這樣的代數(shù)命題等價于一個幾何不等式命題.

例子:

A.3.2 xprove

目的:證明某個具有非負(fù)變量的代數(shù)不等式.

輸入指令:xprove(ineq);或 xprove(ineq，［ineqs］);

指令中各項的含義如下.

ineq:一個待證的代數(shù)不等式，它的所有變量都取非負(fù)值.

ineqs:作為假設(shè)條件的一組代數(shù)不等式，其中所有變量都取非負(fù)值.

需要注意的是:

1)待證的代數(shù)不等式必須是“＜=”型或者“＞=”型，而且作為假設(shè)條件的不等式組ineqs定義一個開集或者一個開集加上它的全部或部份邊界(由于后一限制，當(dāng)原問題的假設(shè)條件中含有某個等式P=Q時，必須用消元的方法去掉等式并降低整個問題的維數(shù)，絕不能簡單地用2個不等式P＞=Q，P＜=Q代替).

2)其假設(shè)ineqs和結(jié)論ineq中只出現(xiàn)有理函數(shù)和根式.

3)“所有變量非負(fù)”在此是默認(rèn)的，不必寫入假設(shè)條件中.

例子:

A.3.3 yprove

目的:證明某個代數(shù)不等式.

輸入指令:yprove(ineq);或 yprove(ineq，［ineqs］);

指令中各項的含義如下.

ineq:一個待證的代數(shù)不等式.

ineqs:作為假設(shè)條件的一組代數(shù)不等式.

需要注意的是:

1)待證的代數(shù)不等式必須“＜=”型或者“＞=”型，而且作為假設(shè)條件的不等式組ineqs定義一個開集或者一個開集加上它的全部或部份邊界(由于后一限制，當(dāng)原問題的假設(shè)條件中含有某個等式P=Q時，必須用消元的方法去掉等式并降低整個問題的維數(shù)，絕不能簡單地用2個不等式P＞=Q，P＜=Q代替).

2)其假設(shè)ineqs和結(jié)論ineq中只出現(xiàn)有理函數(shù)和根式.

例子:

A.3.4 sprove

目的:證明某個具有非負(fù)變量的對稱的多項式不等式.

輸入指令:sprove(ineq);

ineq:一個待證的具有非負(fù)變量的對稱的多項式不等式.

“非負(fù)變量”在此是默認(rèn)的.

目前BOTTEMA尚未考慮另加約束條件的sprove.

A.4 關(guān)于全局優(yōu)化的主要指令及其例解(略)

由于本文并未涉及BOTTEMA的全局優(yōu)化指令，因此這里省略了BOTTEMA關(guān)于全局優(yōu)化的主要函數(shù)功能及其指令例解的介紹，感興趣的讀者可參見文獻(xiàn)［1］.

附錄B 文獻(xiàn)［37］中例子的 BOTTEMA機(jī)器證明指令

上述所有指令耗用的計算機(jī)CPU時間均在秒級范圍之內(nèi).

［1］楊路，夏壁燦.不等式機(jī)器證明與自動發(fā)現(xiàn):數(shù)學(xué)機(jī)械化叢書［M］.北京:科學(xué)出版社，2008.

［2］TARSKI A.A decision method for elementary algebra and geometry［M］.Berkeley，USA:The University of California Press，1951.

［3］吳文俊.初等幾何判定問題與機(jī)械化證明［J］.中國科學(xué):數(shù)學(xué)，1977，20(6):507－516.

WU Wenjun.On the decision problem and mechanization of theorem－proving in elementary－geometry［J］.Science China Mathemation，1977，20(6):507－516.

［4］吳文俊.幾何定理機(jī)器證明的基本原理［M］.北京:科學(xué)出版社，1984.

［5］吳文俊.數(shù)學(xué)機(jī)械化:數(shù)學(xué)機(jī)械化叢書［M］.北京:科學(xué)出版社，2003.

［6］楊路，張景中，侯曉榮.非線性代數(shù)方程組與機(jī)器證明:非線性科學(xué)叢書［M］.上海:上?？茖W(xué)教育出版社，1996.

［7］ARNON D S，COLLINS G E，MCCALLUM S.Cylindrical algebraic decomposition I:the basic algorithm［J］.SIAM Journal on Computing，1984，13(4):865－877.

［8］ARNON D S，COLLINS G E，MCCALLUM S.Cylindrical algebraic decomposition II:an adjacency algorithm for the plane［J］.SIAM Journal on Computing，1984，13(4):878－889.

［9］BROWN C W.Simple CAD construction and its applications［J］.Journal of Symbolic Computation，2001，31(5):521－547.

［10］COLLINS G E.Quantifier elimination for real closed fields by cylindrical algebraic decomposition［C］//Automata Theory and Formal Languages.Kaiserslautern，Germany，1975:134－183.

［11］COLLINS G E，HONG H.Partial cylindrical algebraic decomposition for quantifier elimination［J］.Journal of Symbolic Computation，1991，12(3):299－328.

［12］CHOU S C.Mechanical geometry theorem proving［M］.Dordrecht， Holland:D.Reidel Publishing Company，1988.

［13］CHOU S C，ZHANG J Z，GAO X S.Machine proofs in geometry:automated production of readable proofs for geometry theorems［M］.Singapore:World Scientific，1994.

［14］楊路，侯曉榮，曾振柄.多項式的完全判別系統(tǒng)［J］.中國科學(xué):E 輯，1996，26(5):424－441.

YANG Lu，HOU Xiaorong，ZENG Zhenbing.A complete discrimination system for polynomials［J］.Science in China:Series E，1996，26(5):424－441.

［15］楊路.不等式機(jī)器證明的降維算法與通用程序［J］.高技術(shù)通訊，1998，8(7):20－25.

YANG Lu.A dimension－decreasing algorithm with generic program for automated inequalities proving［J］.High Technology Letters，1998，8(7):20－25.

［16］YANG Lu.Practical automated reasoning on inequalities:generic programs for inequality proving and discovering［C］//Proceedings of the Third Asian Technology Conference in Mathematics.Tsukuba，Japan，1998:24－35.

［17］YANG Lu.Recent advances in automated theorem proving on inequalities［J］.Journal of Computer Science and Technology，1999，14(5):434－446.

［18］楊路，夏時洪.一類構(gòu)造性幾何不等式的機(jī)器證明［J］.計算機(jī)學(xué)報，2003，26(7):769－778.

YANG Lu，XIA Shihong.Automated proving for a class of constructive geometric inequalities［J］.Chinese Journal of Computer，2003，26(7):769－778.

［19］YANG Lu，ZHANG Ju.A practical program of automated proving for a class of geometric inequalities［C］//The Third International Workshop on Automated Deduction in Geometry.London，UK:Springer－Verlag，2001:41－57.

［20］楊路，侯曉榮，夏壁燦.自動發(fā)現(xiàn)不等式型定理的一個完備算法［J］.中國科學(xué):E輯，2001，31(3):424－441.

YANG Lu，HOU Xiaorong，XIA Bican.A complete algorithm for automated discovering of a class of inequality－type theorems［J］.Science in China:Series E，2001，31(3):424－441.

［21］DOLZMANN A，STURM T.REDLOG:computer algebra meets computer logic［J］.ACM SIGSAM Bulletin，1997，31(2):2－9.

［22］BOTTEMA O，DORDEVIC R Z，JANIC R R，et al.Geometric inequlities［M］.Groningen，The Netherlands:Wolters－Noordhoff Publishing，1969.

［23］GERHOLD S，KAUERS M.A procedure for proving special function inequalities involving a discrete parameter［C］//Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation.New York，USA:ACM Press，2005:156－162.

［24］GERHOLD S，KAUERS M.A computer proof of Turán inequality［J］.Journal of Inequalities in Pure and Applied Mathematics，2006，7(2):Article 42.

［25］KAUERS M.Computer proofs for polynomials identities in arbitrary many variables［C］//Proceedings of the 2004 International Smposium on Symbolic and Agebraic Cmputation.New York，USA:ACM Press，2004:199－204.

［26］楊路，姚勇，馮勇.Tarski模型外的一類機(jī)器可判定問題［J］.中國科學(xué):A 輯，2007，37(5):513－522.

YANG Lu，YAO Yong，F(xiàn)ENG Yong.A class of machine determination problem besides the Tarski model［J］.Science China:Series A，2007，37(5):513－522.

［27］YANG Lu，YU Wensheng，YUAN Ruyi.Mechanical decision for a class of intergral inequalities［J］.Science China Information Sciences，2010，53(9):1800－1815.

［28］HARDY G H，LITTLEWOOD J E，POLYA G.Inequalities［M］.Cambridge，UK:Cambridge University Press，1988.

［29］MARSHALL A W，OLKIN I.Inequalities:theory of majorization and its applications［M］.New York，USA:Academic Press，1979.

［30］MITRINOVIC D S.Elementary inequlities［M］.Groningon，The Netherlands:P.Noordhoff Ltd.，1964.

［31］MITRINOVIC D S，VASIC P M.Analytic inequalities［M］.Berlin，Germany:Springer，1970.

［32］張福春，李姿霖.不等式之基本解題方法［J］.數(shù)學(xué)傳播，2007，31(2):38－61.

ZHANG Fuchun，LI Zilin.The basic problem－solving methods for inequality［J］.Mathematical Communication，2007，31(2):38－61.

［33］匡繼昌.常用不等式［M］.4版.濟(jì)南:山東科學(xué)技術(shù)出版社，2010.

［34］ACZEL J.Some general methods in the theory of functional equations in one variable:new applications of functional equations［J］.Uspekhi Matematicheskikh Nauk，1956，11(3):3－68.

［35］ACZEL J，VARGA O.Bemerkung zur Cayley－Kleinschen Massbestimmung［J］.Punl Math，1955，4:3－15.

［36］NANJUNDIAH T S.Problem 10347［J］.The American Mathematical Monthly，1993，100(10):951－952.

［37］BEESACK P R.On certain discrete inequalities involving partial sums［J］.Canadian Journal of Mathematics，1969，21:222－234.

楊路，男，1936年生，教授，博士生導(dǎo)師，主要研究方向為定理機(jī)器證明、數(shù)學(xué)機(jī)械化與推理自動化、計算代數(shù)幾何特別是計算實代數(shù)幾何及其在信息技術(shù)領(lǐng)域的應(yīng)用等.

郁文生，男，1967年生，教授，博士生導(dǎo)師，博士，主要研究方向為魯棒控制、泛函微分方程理論、符號計算和實代數(shù)理論及應(yīng)用、系統(tǒng)全局優(yōu)化、數(shù)學(xué)機(jī)械化與推理自動化及其在信息技術(shù)領(lǐng)域的應(yīng)用等.

Automated proving of some fundamental applied inequalities

YANG Lu，YU Wensheng
(Shanghai Key Laboratory of Trustworthy Computing，East China Normal University，Shanghai 200062，China)

The automated proving of inequalities is always a difficult and hot topic in the field of intelligence systems.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－geometricharmonic 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.

fundamental applied inequalities;automated proving;inequality－proving package BOTTEMA;Tarski model

TP181

A

1673－4785(2011)05－0377－14

10.3969/j.issn.1673－4785.2011.05.001

2011－04－13.

國家自然科學(xué)基金資助項目(61070048，60874010);國家自然科學(xué)基金委員會創(chuàng)新研究群體科學(xué)基金資助項目(61021004);國家“863”計劃資助項目(2011AA010101);國家“973”計 劃 資 助 項 目 (2011CB302802，2011CB302400);上海市重點(diǎn)學(xué)科建設(shè)資助項目(B412);上海市教育委員會科研創(chuàng)新資助項目(11ZZ37).

郁文生.E－mail:wsyu@sei.ecnu.edu.cn.