常用基本不等式的機器證明

楊路，郁文生

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

常用基本不等式的機器證明

楊路，郁文生

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

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

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

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

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

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

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

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

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

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

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

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

1 常用基本不等式的機器證明

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

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

1.1 算術、幾何與調和平均不等式的機器證明

算術、幾何與調和平均不等式(arithmetic－geometric－harmonic inequality) 設 a1，a2，…，an為 n 個正實數，則

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

將式(2)取倒數即得

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

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

上式可以改寫成:

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

這時引進新的變元r，考慮命題:

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

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

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

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

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

如果考慮如下的算術與調和平均不等式:

類似上面的討論，引進新變元A、B，執行BOTTEMA的xprove指令:

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

1.2 Cauchy不等式的機器證明

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

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

容易驗證φ1和φ2成立.按照數學歸納法，需要證明

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

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

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

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

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

1.3 排序不等式的機器證明

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

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

排序不等式可以導出許多不等式，例如算術與幾何平均不等式、Cauchy不等式及下一小節的Chebyshev不等式等.

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

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

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

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

這里調用BOTTEMA的yprove指令，只是為了說明本文機器證明方法的統一性.這即完成了“順序和大于等于亂序和”的證明.

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

1.4 Chebyshev不等式的機器證明

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

Chebyshev不等式當然可以由排序不等式證得，下面給出基于BOTTEMA的證明方法.為使機器證明更好地體現Chebyshev不等式前提中的單調性條件，引進比“單調數列”更廣泛的所謂“均和單調數列”的概念.

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

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

顯然，單調遞增的數列是均和不減的，單調遞減的數列是均和不增的.

先證

注意到“均和單調數列”的定義，只需執行BOTTEMA的yprove指令:

為證

式(14)即可得證.

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

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

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

證明根據題設，不妨令

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

化簡整理得

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

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

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

證明根據題設，不妨令

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

化簡整理，得

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

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

1.5 Bernoulli不等式的機器證明

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

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

成立.

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

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

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

使用BOTTEMA的xprove指令:

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

使用BOTTEMA的xprove指令:

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

于是，使用BOTTEMA的xprove指令:

使用BOTTEMA的xprove指令:

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

1.6 三角形不等式的機器證明

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

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

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

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

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

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

1.7 Jensen不等式的機器證明

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

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

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

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

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

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

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

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

于是，自然有

上式當然也可通過執行BOTTEMA的yprove指令:

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

2 更多的實例

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

例 1［1，23］證明文獻［30］中的一個不等式:

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

使用BOTTEMA的xprove指令:

可在幾秒內證明上式成立.

例 2［1］證明

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

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

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

執行指令:

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

例 3［1，24］用機器證明 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)顯然為假，于是需要添加一些條件.根據Legendre多項式的遞歸性質:

那么，修改后的量詞消去問題變為:

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

例 4［23］證明

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

例5［23］證明文獻［30］中3.27的一個不等式:

式中:是尋常的二項系數，即

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

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

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

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

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

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

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

式中:R表示實數集合.

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

計算機在2 s內即能證明式(33)成立.

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

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

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

例9［23］證明文獻［30］中4.15的一個相關不等式:

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

計算機在2 s內證明式(35)成立.

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

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

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

使用BOTTEMA的xprove指令:

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

例11［23］證明文獻［30］中7.31與7.32出現的相關不等式:

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

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

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

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

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

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

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

k

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

依次執行如下BOTTEMA的xprove指令:

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

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

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

例14［23］考慮文獻［30］中5.16的不等式:

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

計算機在數秒內即驗證了式(41)成立.

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

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

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

可將式(42)化簡為

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

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

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

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

式中:xi≥0，n≥1.

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

另外，文獻［23］還討論了如下的不等式:

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

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

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

3結論

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

幾點注記如下.

1)BOTTEMA是一個高效能的程序，通過反復試驗能夠證明和發現許多過去靠計算機難以證明的不等式.結合人工證明和巧妙的代換方法，可充分發揮BOTTEMA的效能.

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

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

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

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

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

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

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

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

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

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

A.1 如何安裝和運行BOTTEMA

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

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

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

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

注意標點“、”是不能省略的，然后您就可以執行BOTTEMA的所有指令，使用其所有功能.

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

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

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

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

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

R:外接圓半徑.

r:內切圓半徑.

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

ha、hb、hc:各邊對應的高.

ma、mb、mc:各邊對應的中線長.

wa、wb、wc:各邊對應的內角平分線長

S:三角形的面積.

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

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

A、B、C:三角形的各內角.

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

abs():絕對值.

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

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

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

A.3.1 prove

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

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

指令中各項的含義如下.

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

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

需要注意的是:

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

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

例子:

A.3.2 xprove

目的:證明某個具有非負變量的代數不等式.

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

指令中各項的含義如下.

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

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

需要注意的是:

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

2)其假設ineqs和結論ineq中只出現有理函數和根式.

3)“所有變量非負”在此是默認的，不必寫入假設條件中.

例子:

A.3.3 yprove

目的:證明某個代數不等式.

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

指令中各項的含義如下.

ineq:一個待證的代數不等式.

ineqs:作為假設條件的一組代數不等式.

需要注意的是:

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

2)其假設ineqs和結論ineq中只出現有理函數和根式.

例子:

A.3.4 sprove

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

輸入指令:sprove(ineq);

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

“非負變量”在此是默認的.

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

A.4 關于全局優化的主要指令及其例解(略)

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

附錄B 文獻［37］中例子的 BOTTEMA機器證明指令

上述所有指令耗用的計算機CPU時間均在秒級范圍之內.

［1］楊路，夏壁燦.不等式機器證明與自動發現:數學機械化叢書［M］.北京:科學出版社，2008.

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

［3］吳文俊.初等幾何判定問題與機械化證明［J］.中國科學:數學，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］吳文俊.幾何定理機器證明的基本原理［M］.北京:科學出版社，1984.

［5］吳文俊.數學機械化:數學機械化叢書［M］.北京:科學出版社，2003.

［6］楊路，張景中，侯曉榮.非線性代數方程組與機器證明:非線性科學叢書［M］.上海:上海科學教育出版社，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］楊路，侯曉榮，曾振柄.多項式的完全判別系統［J］.中國科學: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］.高技術通訊，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］楊路，夏時洪.一類構造性幾何不等式的機器證明［J］.計算機學報，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］楊路，侯曉榮，夏壁燦.自動發現不等式型定理的一個完備算法［J］.中國科學: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］.中國科學:A 輯，2007，37(5):513－522.

YANG Lu，YAO Yong，FENG 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］.數學傳播，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版.濟南:山東科學技術出版社，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年生，教授，博士生導師，主要研究方向為定理機器證明、數學機械化與推理自動化、計算代數幾何特別是計算實代數幾何及其在信息技術領域的應用等.

郁文生，男，1967年生，教授，博士生導師，博士，主要研究方向為魯棒控制、泛函微分方程理論、符號計算和實代數理論及應用、系統全局優化、數學機械化與推理自動化及其在信息技術領域的應用等.

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.

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

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