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

楊路，郁文生

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

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

楊路，郁文生

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

上式可以改寫(xiě)成:

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

這時(shí)引進(jìn)新的變?cè)猺，考慮命題:

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

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

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

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

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

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

類(lèi)似上面的討論，引進(jìn)新變?cè)狝、B，執(zhí)行BOTTEMA的xprove指令:

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

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

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

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

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

這時(shí)引進(jìn)新的變?cè)猺、s、t、x、y，考慮命題:

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

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

不過(guò)顯而易見(jiàn)，如果已經(jīng)證明Cauchy不等式對(duì)于所有的xk≥0，yk≥0 成立，那么當(dāng)xk、yk為一般實(shí)數(shù)時(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ù)有序數(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中存在某個(gè)m≠n，使得bn與am搭配，即在S中含有項(xiàng)ambn(m≠n).因此，只要

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

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

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

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

仿照上述過(guò)程可以給出“亂序和大于等于逆序和”的機(jī)器證明，當(dāng)然，也可直接利用“順序和大于等于亂序和”來(lái)證明“亂序和大于等于逆序和”，這只需對(duì)2組實(shí)數(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í)數(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，…}，若滿(mǎn)足條件:

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

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

先證

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

為證

式(14)即可得證.

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

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

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

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

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

化簡(jiǎn)整理得

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

類(lèi)似地，可以證明如下的命題.

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

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

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

化簡(jiǎn)整理，得

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

命題1和命題2的證明根本無(wú)需BOTTEMA，在任何符號(hào)計(jì)算軟件平臺(tái)上都容易驗(yàn)證.

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

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

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

成立.

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

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

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

使用BOTTEMA的xprove指令:

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

使用BOTTEMA的xprove指令:

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

于是，使用BOTTEMA的xprove指令:

使用BOTTEMA的xprove指令:

最后，對(duì)于Bernoulli不等式(21)或(22)在r取任意實(shí)數(shù)的情形，可由有理數(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 個(gè)向量，則

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

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

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

對(duì)于式(24)左邊的不等式，可以對(duì)c=a+b和d=－b應(yīng)用式(24)右邊的不等式即可，也可以類(lèi)似于式(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)的不等式變號(hào).

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

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

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

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

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

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

于是，自然有

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

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

2 更多的實(shí)例

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

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

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

使用BOTTEMA的xprove指令:

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

例 2［1］證明

對(duì)一切滿(mǎn)足下列條件的實(shí)數(shù)xk、yk成立.

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

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

執(zhí)行指令:

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

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

式中:Pn(x)表示第n個(gè)Legendre多項(xiàng)式.

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

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

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

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

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

例 4［23］證明

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

使用BOTTEMA的xprove指令:

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

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

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

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

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

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

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

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

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

k

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

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

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

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

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

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

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

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

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

可將原不等式化為如下的等價(jià)形式:

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

可將式(42)化簡(jiǎn)為

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

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

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

該不等式可等價(jià)地化為如下的多項(xiàng)式不等式［27］:

式中:xi≥0，n≥1.

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

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

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

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

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

3結(jié)論

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

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

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

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

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

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

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

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

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

附錄A BOTTEMA簡(jiǎn)易使用指南［1］

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

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

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

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

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

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

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

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

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

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

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

a、b、c:三角形各邊之長(zhǎng).

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

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

R:外接圓半徑.

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

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

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

ma、mb、mc:各邊對(duì)應(yīng)的中線(xiàn)長(zhǎng).

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

S:三角形的面積.

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

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

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

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

abs():絕對(duì)值.

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

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

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

A.3.1 prove

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

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

指令中各項(xiàng)的含義如下.

ineq:一個(gè)待證的不等式，它是用上面列表中的幾何不變量來(lái)表述的.

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

需要注意的是:

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

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

例子:

A.3.2 xprove

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

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

指令中各項(xiàng)的含義如下.

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

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

需要注意的是:

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

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

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

例子:

A.3.3 yprove

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

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

指令中各項(xiàng)的含義如下.

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

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

需要注意的是:

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

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

例子:

A.3.4 sprove

目的:證明某個(gè)具有非負(fù)變量的對(duì)稱(chēng)的多項(xiàng)式不等式.

輸入指令:sprove(ineq);

ineq:一個(gè)待證的具有非負(fù)變量的對(duì)稱(chēng)的多項(xiàng)式不等式.

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

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

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

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

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

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

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

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

［3］吳文俊.初等幾何判定問(wèn)題與機(jī)械化證明［J］.中國(guó)科學(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ī)械化叢書(shū)［M］.北京:科學(xué)出版社，2003.

［6］楊路，張景中，侯曉榮.非線(xiàn)性代數(shù)方程組與機(jī)器證明:非線(xiàn)性科學(xué)叢書(shū)［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］楊路，侯曉榮，曾振柄.多項(xiàng)式的完全判別系統(tǒng)［J］.中國(guó)科學(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］楊路，夏時(shí)洪.一類(lèi)構(gòu)造性幾何不等式的機(jī)器證明［J］.計(jì)算機(jī)學(xué)報(bào)，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］楊路，侯曉榮，夏壁燦.自動(dòng)發(fā)現(xiàn)不等式型定理的一個(gè)完備算法［J］.中國(guó)科學(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模型外的一類(lèi)機(jī)器可判定問(wèn)題［J］.中國(guó)科學(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)師，主要研究方向?yàn)槎ɡ頇C(jī)器證明、數(shù)學(xué)機(jī)械化與推理自動(dòng)化、計(jì)算代數(shù)幾何特別是計(jì)算實(shí)代數(shù)幾何及其在信息技術(shù)領(lǐng)域的應(yīng)用等.

郁文生，男，1967年生，教授，博士生導(dǎo)師，博士，主要研究方向?yàn)轸敯艨刂?、泛函微分方程理論、符?hào)計(jì)算和實(shí)代數(shù)理論及應(yīng)用、系統(tǒng)全局優(yōu)化、數(shù)學(xué)機(jī)械化與推理自動(dòng)化及其在信息技術(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.

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

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