陳世平，陳 果

（1.中國民航飛行學(xué)院德陽校區(qū)-四川省商貿(mào)學(xué)校，四川 德陽 618000；2.西南科技大學(xué)信息工程學(xué)院，四川 綿陽 612000）

0 引 言

Nishizawa 證明了[10]：

Branko Male?evic 等證明了文獻(xiàn)[10]提出的公開問題[11]：

文獻(xiàn)[12-17]討論了形如f（x，trans1（x），…，transn（x））＞0 的超越多項(xiàng)式不等式的機(jī)器證明，其中f（x，x1，…，xn）是n＋1 元多項(xiàng)式，trans1（x）可以是初等超越函數(shù)，如sin x、cos x、tan x、arcsin x、arccos x、arctan x、ex、ln x 等，也可以是形如trans1（trans2（x））的復(fù)合函數(shù)，利用一次或多次Taylor 替換，目標(biāo)不等式的證明轉(zhuǎn)化為一系列單變量的多項(xiàng)式不等式的驗(yàn)證，然后由代數(shù)不等式證明軟件BOTTEMA 完成.算法對于常見的超越多項(xiàng)式不等式非常有效，而且是“可讀的”，可以輸出能夠理解的證明過程.這種方案被稱為逐次Taylor 替換法.

本文的目的是討論定理2 中不等式的機(jī)器證明，這是一個(gè)比文獻(xiàn)[12-17]中引用的例子更復(fù)雜、超越多項(xiàng)式不等式范圍外形如sin（x）/x＞u（x）v(x)的冪指函數(shù)不等式問題，運(yùn)用逐次Taylor 替換并結(jié)合人工證明和巧妙的變量代換，實(shí)現(xiàn)了該不等式的機(jī)器證明.通過與文獻(xiàn)[11]不同的途徑，也證明了文獻(xiàn)[10]提出的公開問題，盡管結(jié)論是已知的結(jié)果，但方法本身對于同類不等式具有示范性.

此外，算法輸出的證明過程中除了有的需要判定其正定性的一元有理多項(xiàng)式次數(shù)較高從而驗(yàn)證計(jì)算量較大外，其余內(nèi)容都容易“手工”驗(yàn)算.

1 逐次Taylor替換

不等式的自動證明問題，一直以來都是數(shù)學(xué)機(jī)械化和自動推理領(lǐng)域研究熱點(diǎn)和難點(diǎn)問題.近年來，代數(shù)不等式的自動證明吸引了大批學(xué)者研究，也取得了豐富的成果，已有專著《不等式機(jī)器證明與自動發(fā)現(xiàn)》問世，特別是楊路教授提出了降維算法，據(jù)之編制的通用程序BOTTEMA 能夠成批驗(yàn)證不等式，但BOTTEMA 只能處理代數(shù)不等式或先把幾何不等式轉(zhuǎn)化為代數(shù)不等式，尚不能解決一般的超越不等式自動證明問題[18-22].當(dāng)然關(guān)于超越不等式已有了大量的研究成果和證明方法，但這些成果和方法尚不能適應(yīng)數(shù)學(xué)機(jī)械化和推理自動化的需要，故有必要對此類不等式的自動證明進(jìn)行專門的研究，探索新的算法.

1.1 Taylor替換

給定（n＋1）元實(shí)系數(shù)多項(xiàng)式環(huán)R[x，x1，…，xn]，定義該環(huán)上一個(gè)映射：hom:f（x，x1，…，xn）→F（x），將變量xi用某個(gè)超越函數(shù)transi（x）代替.

定義1.1 給定（n＋1）元實(shí)系數(shù)多項(xiàng)式f（x，x1，…，xn），它在映射hom 下的像F（x）=hom（f）=f（x，trans1（x），…，transn（x））稱為超越函數(shù)多項(xiàng)式，稱transi（x）為其超越因子.

如x＋sin（x）、x＋cos（sqrt（x））、x＋esin(x)、x＋arctan（x）-arcsin（x）都是超越函數(shù)多項(xiàng)式，sin（x）、cos（sqrt（x））、esin(x)、arctan（x）、arcsin（x）就是函數(shù)的超越因子.

定義 1.2 對于超越函數(shù) F（x），在某個(gè)區(qū)間 I，如果有代數(shù)函數(shù)列{T_min（n，F(xiàn)）}和{T_max（n，F(xiàn)）}，存在自然數(shù) n0，當(dāng) n≥n0時(shí)，滿足：

1）T_min（n＋1，F(xiàn)）＞T_min（n，F(xiàn)），且當(dāng) n→∞ 時(shí)，T_min（n，F(xiàn)）→F（x）；

2）T_max（n＋1，F(xiàn)）＜T_max（n，F(xiàn)），且當(dāng) n→∞ 時(shí)，T_max（n，F(xiàn)）→F（x）.

我們稱{T_min（n，F(xiàn)）}和{T_max（n，F(xiàn)）}為 F（x）在區(qū)間 I 的下限多項(xiàng)式列和上限多項(xiàng)式列，T_min（n，F(xiàn)）為 F（x）的下限多項(xiàng)式，T_max（n，F(xiàn)）為 F（x）的上限多項(xiàng)式，n0稱為臨界值.

顯然，F(xiàn)（x）的下限多項(xiàng)式和上限多項(xiàng)式滿足：

T_min（n0，F(xiàn)）（x）＜T_min（n0＋1，F(xiàn)）（x）＜T_min（n0＋2，F(xiàn)）（x）＜…＜F（x）＜…＜T_max（n0＋2，F(xiàn)）（x）＜T_max（n0＋1，F(xiàn)）（x）＜T_max（n0，F(xiàn)）（x），也就是說若 F（x）存在有下限多項(xiàng)式列和上限多項(xiàng)式列，則有一個(gè)多項(xiàng)式套來逼近 F（x）:（T_min（n0，F(xiàn)）（x），T_max（n0，F(xiàn)）（x））?（T_min（n0＋1，F(xiàn)）（x），T_max（n0＋1，F(xiàn)）（x））?（T_min（n0＋2，F(xiàn)）（x），T_max（n0＋2，F(xiàn)）（x））?……?{F（x）}.

下面我們討論如何計(jì)算或構(gòu)造超越函數(shù)多項(xiàng)式F（x）=f（x，trans（x））的下限多項(xiàng)式和上限多項(xiàng)式（其中f（x，y）為二元多項(xiàng)式）.

為方便，我們將函數(shù)f（x）在0 點(diǎn)的Taylor 展開式中的前n 項(xiàng)之和記為taylor（f，n）.

定義1.3 如果超越函數(shù)f（x）在某個(gè)區(qū)間（0，T］滿足以下條件：（1）大于0；（2）在0 點(diǎn)的Taylor 展開式收斂于f（x）；（3）taylor（f，n）可以表示為交錯(cuò)級數(shù)f1（x）-f2（x）＋f3（x）＋…＋（-1）n-1fn（x），其中fn（x）=An*x＾mn，0＜An≤1，mn-1＜mn；（4）存在常數(shù)n0，當(dāng)n≥n0時(shí)，taylor（f，n）＞0，fn（x）＞fn＋1（x）＞0.我們稱f（x）在區(qū)間（0，T］內(nèi)可以規(guī)范展開，常數(shù)n0稱為其臨界值.若還滿足An≤1/（n-1）!，則稱f（x）在區(qū)間（0，T］內(nèi)可以強(qiáng)規(guī)范展開.

常見的基本初等超越函數(shù)大都可以在相應(yīng)的區(qū)間內(nèi)規(guī)范展開：

arctan（x）=x-x3/3＋x5/5-x7/7＋…＋（-1）n-1x2n-1/（2n-1）＋……在區(qū)間（0，1］可以規(guī)范展開，臨界值n0=1；

e-x=1-x＋x2/2!-x3/3!＋…＋（-x）n-1/（n-1）?。?，在區(qū)間（0，T］（T 為任意正數(shù)，下同）可以規(guī)范展開，臨界值n0=min{n∈N，當(dāng)0＜x≤T 時(shí)taylor（e-x，n）＞0，taylor（e-x，n＋1）＞0，n＞T}；

ln（1＋x）=x-x2/2＋x3/3-……＋在區(qū)間（0，1］可以規(guī)范展開，臨界值n0=1；

sin（x）=x-x3/3!＋x5/5!-……＋在區(qū)間（0，T］可以規(guī)范展開，其中臨界值n0=min{n∈N，當(dāng)0＜x≤T 時(shí)taylor（sin（x），n）＞0，taylor（sin（x），n＋1）＞0 且2n（2n＋1）＞T2}，特別地，當(dāng)時(shí)，n0=1；

cos（x）=1-x2/2!＋x4/4!-……＋在區(qū)間（0，T］可以規(guī)范展開，其中臨界值n0=min{n∈N，當(dāng)0＜x≤T 時(shí)taylor（cos（x），n）＞0，taylor（cos（x），n＋1）＞0 且 2n（2n-1）＞T2}.我們注意到，當(dāng)時(shí)，taylor（cos（x），2n）＜cos（x）=0，所以 cos（x）在內(nèi)不能規(guī)范展開；

（1＋x）a=1＋ax＋a（a-1）x2/2!＋a（a-1）（a-2）x3/3!＋C（a，n）xn＋…，在區(qū)間（0，1）可以規(guī)范展開（其中 C（a，n）=a（a-1）（a-2）…（a-n＋1））.當(dāng) 0＜a＜1 時(shí)，n0=1（展開式中f1（x）=1＋ax）.

其中 e-x、sin（x）、cos（x）在相應(yīng)區(qū)間內(nèi)還可強(qiáng)規(guī)范展開.

也有一些基本初等超越函數(shù)不能規(guī)范展開，如：

ln（1-x）=-x-x2/2-x3/3-……-xk/k-……（0＜x＜1）；

tan（x）=ΣB2n（-4）n（1-4n）x(2n-1)/（2n）!=x＋（1/3）x3＋（2/15）x5＋（17/315）x7＋（62/2835）x9＋……

引理1.1 如果f（x）區(qū)間I 可以規(guī)范展開，臨界值為n0，則當(dāng)n＞n0時(shí)，在區(qū)間I 上

1）taylor（f，2n-2）＜taylor（f，2n）＜f（x）；

2）taylor（f，2n-1）＞taylor（f，2n＋1）＞f（x）；

3）當(dāng)n→∞時(shí)，taylor（f，n）→f（x）.

為方便，引入如下記號：

acrtan_max（x，n）=taylor（arctan（x），2n＋1），arctan_min（x，n）=taylor（arctan（x），2n），則當(dāng) x∈（0，1］，對任意 n∈N，arctan_max（x，n）＞arctan（x）＞arctan_min（x，n）；

ln_max（x，n）=taylor（ln（1＋x），2n＋1），ln_min（x，n）=taylor（ln（1＋x），2n），則當(dāng)x∈（0，1），對任意 n∈N，ln_max（x，n）＞ln（1＋x）＞ln_min（x，n）；

sin_max（x，n）=taylor（sin（x），2n＋1），sin_min（x，n）=taylor（sin（x），2n），則當(dāng)x∈對任意 n∈N，sin_max（x，n）＞sin（x）＞sin_min（x，n）；

cos_max（x，n）=taylor（cos（x），2n＋1），cos_min（x，n）=taylor（cos（x），2n），則當(dāng)對任意 n∈N，cos_max（x，n）＞cos（x）＞cos_min（x，n）；

用f＋和f-分別表示多項(xiàng)式f 展開后的正項(xiàng)和負(fù)項(xiàng)之和，顯然f=f＋＋f-，并且下面的引理成立：

引理1.2 假設(shè)實(shí)函數(shù)T1（y）＞0，T2（y）＞0 且T1（y）＜x＜T2（y），則

f＋（T1（y），y）＋f-（T2（y），y）＜f（x，y）＜f＋（T2（y），y）＋f-（T1（y），y）.

定理1.1 F（x）=f（x，trans（x）），trans（x）在區(qū)間I 可以規(guī)范展開，則對任意n∈N，

T_max（n，F(xiàn)）=f＋（x，taylor（trans（x），2n-1））＋f-（x，taylor（trans（x），2n））為 F（x）的上限多項(xiàng)式；

T_min（n，F(xiàn)）=f＋（x，taylor（trans（x），2n））＋f-（x，taylor（trans（x），2n-1））為 F（x）的下限多項(xiàng)式.

定理 1.2 設(shè){T_min（n，F(xiàn)）}和{T_max（n，F(xiàn)）}分別是超越函數(shù)多項(xiàng)式 F（x）在區(qū)間 I 的下限多項(xiàng)式列和上限多項(xiàng)式列，則在相應(yīng)區(qū)間內(nèi)，

1）若存在 n0使得 T_min（n0，F(xiàn)）≥0 成立，則 F（x）＞0 成立；

2）若存在 n0使得 T_max（n0，F(xiàn)）≤0 成立，則 F（x）＜0 成立；

3）若存在 n0使得 T_max（n0，F(xiàn)）＞0 和 T_min（n0，F(xiàn)）＜0 都不成立，則 F（x）在區(qū)間 I的符號不固定.

上述方案運(yùn)用Taylor 展開式構(gòu)造超越函數(shù)多項(xiàng)式的上下限多項(xiàng)式列，建立一個(gè)逼近目標(biāo)函數(shù)的一元多項(xiàng)式套，從而將目標(biāo)不等式的證明轉(zhuǎn)化為一系列的一元多項(xiàng)式不等式的驗(yàn)證，我們將這種方案稱為Taylor 替換法.

1.2 逐次Taylor替換

一般的超越函數(shù)多項(xiàng)式可能包含多個(gè)超越因子，超越因子可能還是由超越函數(shù)或代數(shù)函數(shù)復(fù)合而成，經(jīng)過一次Taylor 替換后的函數(shù)可能還是包含超越因子，還需要再次甚至多次的Taylor 替換.我們以超越函數(shù)多項(xiàng)式F（x）=f（x，trans1（x），trans2（x））和F（x）=f（x，trans1（trans2（x）））為例來描述這個(gè)過程：

1、F（x）=f（x，trans1（x），trans2（x）），其中超越函數(shù)trans1（x）、trans2（x）在區(qū)間I 內(nèi)可以規(guī)范展開，臨界值分別為n1、n2.

令f1（x，trans2（x），m）=f＋（x，taylor（trans1（x），2*m），trans2（x））＋f-（x，taylor（trans1（x），2*m-1），trans2（x））；

令f2（x，m，n）=f1＋（x，taylor（trans2（x），2*n），m）＋f1-（x，taylor（trans2（x），2*n-1），m）；

顯然當(dāng)m＞n1時(shí)，f1（x，trans2（x），m）＜f（x，trans1（x），trans2（x）），當(dāng)m→∞時(shí)，f1（x，trans2（x），m）→f（x，trans1（x），trans2（x））；

當(dāng)n＞n2時(shí)，對任意m＞n1，f2（x，m，n）＜f1（x，trans2（x），m），當(dāng)n→∞時(shí)，f2（x，m，n）→f1（x，trans2（x），m）；

即當(dāng)m＞n1，n＞n2時(shí)，f2（x，m，n）＜f（x，trans1（x），trans2（x）），當(dāng)m→∞，n→∞時(shí)，f2（x，m，n）→F（x）.

特別地，T_min（n，F(xiàn)）=f2（x，n，n）就是F（x）的下限多項(xiàng)式，{T_min（F，n）}是其下限多項(xiàng)式列，其臨界值n0=max{n1，n2}.

類似的方法可以求得F（x）的上限多項(xiàng)式列.

同樣的方法我們可以計(jì)算含更多“超越因子”形如f（x，trans1（x），trans2（x），trans3（x），…，transm（x））的超越函數(shù)的上下限多項(xiàng)式列.

2、F（x）=f（x，trans1（trans2（x））），其中trans2（x）在區(qū)間I 可以規(guī)范展開，其臨界值為n2，trans2（x）在區(qū)間I 上的值域?yàn)閰^(qū)間J，trans1（x）在J 內(nèi)可以規(guī)范展開，其臨界值為n1.

令trans2（x）=u，得到F1（x，u）=f（x，trans1（u）），

令f1（x，m，u）=f＋（x，taylor（trans1（u），2m））＋f-（x，taylor（trans1（u），2m-1）），

顯然，當(dāng)m＞n1時(shí)f1（x，m，u）＜F1（x，u）=f（x，trans1（u）），且當(dāng)m→∞時(shí)，f1（x，m，u）→F1（x，u）；

若trans2（x）是代數(shù)函數(shù)，則f1（x，m，trans2（x））就是F（x）的下限多項(xiàng)式，否則

令f2（x，m，n）=f1＋（x，m，taylor（trans2（x），2n））＋f1-（x，m，taylor（trans2（x），2n-1）），

當(dāng)n＞n2時(shí)，f2（x，m，n）＜f1（x，m，trans2（x））＜F（x）=f（x，trans1（trans2（x））），且當(dāng)n→∞時(shí)，f2（x，m，n）→f1（x，m，trans2（x））；

從而當(dāng)m→∞，n→∞時(shí)，f2（x，m，n）→F（x）=f（x，trans1（trans2（x）））.

特別地，T_min（F，n）=f2（x，n，n）是F（x）的下限多項(xiàng)式，{T_min（F，n）}是其下限多項(xiàng)式列.其臨界值n0=max{n1，n2}.

類似的方法可以求得F（x）的上限多項(xiàng)式列.

同樣的方法我們可以計(jì)算含形如trans1（trans2（trans3（x）））經(jīng)過更多次復(fù)合而成的超越因子的超越函數(shù)的上下限多項(xiàng)式列.

我們把上述方案稱為逐次Taylor 替換，一個(gè)可以計(jì)算一般超越函數(shù)多項(xiàng)式f（x，trans1（x），…，transn（x））的上下限多項(xiàng)式列的逐次Taylor 替換過程可以遞歸地定義如下：

算法 1.1 STS（Successive Taylor Substitution）

輸入①超越函數(shù)多項(xiàng)式F（x）；②n∈N；

輸出F（x）的下（上）限多項(xiàng)式.

1）若 F（x）為代數(shù)函數(shù)

return[F（x），F(xiàn)（x）]；

算法結(jié)束；

2）設(shè)trans（x）是F（x）的一個(gè)超越因子且可以表示為F（x）=f（x，trans（x））

2.1）若trans（x）在相應(yīng)區(qū)間可以規(guī)范展開，則

f1（x，n）←f＋（x，taylor（trans（x），2n））＋f-（x，taylor（trans（x），2n-1））；

T_min（n，F(xiàn)）←STS（f1（x，n））[1]；

f2（x，n）←f＋（x，taylor（trans（x），2n-1））＋f-（x，taylor（trans（x），2n））；

T_max（n，F(xiàn)）←STS（f2（x，n））[2]；

return[T_min（n，F(xiàn)），T_max（n，F(xiàn)）]；

2.2）若trans（x）具有形如trans1（trans2（x））的復(fù)合形式，令F（x）=f（x，trans1（u）），其中u=trans2（x），假設(shè)trans1（u）在相應(yīng)區(qū)間可以規(guī)范展開.

f1（x，n，u）←f＋（x，taylor（trans1（u），2n））＋f-（x，taylor（trans1（u），2n-1））；

T_min（n，F(xiàn)）←STS（f1（x，n，trans2（x）））[1]；

f2（x，n，u）←f＋（x，taylor（trans1（u），2n-1））＋f-（x，taylor（trans1（u），2n））；

T_max（n，F(xiàn)）←STS（f2（x，n，trans2（x）））[2]；

return[T_min（n，F(xiàn)），T_max（n，F(xiàn)）]；

3）END.

算法STS 還不能直接處理類似tan（x）、ln（1-x）、ex這類不能規(guī)范展開的超越因子，在證明過程中需要結(jié)合人工證明和做一些的變量代換.

超越函數(shù)多項(xiàng)式的“超越因子”還可能就是超越常數(shù)，也需要有理化.本文的處理方法是將超越數(shù)視為一個(gè)超越函數(shù)，構(gòu)造一個(gè)逼近該超越數(shù)的有理數(shù)端點(diǎn)區(qū)間套.比如對于超越數(shù)t，我們構(gòu)造滿足如下性質(zhì)的區(qū)間列{[t1（n），t2（n）]}：

1）t1（1）＜t1（2）＜…＜t1（n）＜…＜t＜…t2（n）＜…t2（2）＜t2（1）；

2）當(dāng)n→∞時(shí)，t1（n）→t，t2（n）→t；

3）端點(diǎn)t1（n）和t2（n）均為有理數(shù).

若f（x，t）是系數(shù)含超越數(shù)t 的一元多項(xiàng)式，則

T_max（n，f）=f＋（x，t1（n））＋f-（x，t2（n））為f（x，t）的上限多項(xiàng)式；

T_min（n，f）=f＋（x，t2（n））＋f-（x，t1（n））為f（x，t）的下限多項(xiàng)式.

輸入：n∈N；

輸出：有理數(shù)端點(diǎn)區(qū)間[t1（n），t2（n）]，滿足：對任意p≤n，t1（1）＜t1（2）＜…＜t1（p）＜＜t2（p）＜…＜t2（2）＜t2（1）；當(dāng)n→∞ 時(shí)，t1（n）→，t2（n）→.

1）t1←16*subs（x=1/5，arctan_min（x，n））-4*subs（x=1/239，acrtan_max（x，n））；

2）t2←16*subs（x=1/5，acrtan_max（x，n））-4*subs（x=1/239，tarctan_min（x，n））；

3）return[t1，t2]；算法結(jié)束.

2 定理2的證明

令f3（x）=numer（f2（x））*denom（f2（x））（其中numer（f（x））和denom（f（x））分別取分式的分子和分母，下同），顯然sgn（f2（x））=sgn（f3（x））.

令g1（x，n）=subs（ln（x/sin（x））=B（x，n），f3＋）＋subs（ln（x/sin（x））=A（x，n），f3-），則對任意n∈N，g1（x，n）＜f3（x）；

令g2（x，n）=numer（g1（x））*denom（g1（x））；

令g3（x，n）=subs（sin（x）=sin_min（x，n），g2＋）＋subs（sin（x）=sin_max（x，n），g2-），則對任意n∈N，g3（x，n）＜g2（x，n）；

令g4（x，n）=subs（cos（x）=cos_min（x，n），g3＋）＋subs（cos（x）=cos_max（x，n），g3-），則對任意n∈N，g4（x，n）＜g3（x，n），此時(shí)g4（x，n）還含有超越數(shù)作為系數(shù)；

令g5（x，n）=subs（=_to_ra（tn）[1]，g4＋）＋subs（=_to_ra（tn）[2]，g4-），則對任意n∈N，g5（x，n）是關(guān)于x 的一元有理多項(xiàng)式，且g5（y，n）＜g4（x，n）＜g3（x，n）＜g2（x，n）；

使用BOTTEMA 的xprove 指令：xprove（g5（x，n）＞0，[x＜_to_rat（n）[2]/3]）， 當(dāng)n=5 時(shí)，不等式g5（x，n）＞0 成立，即當(dāng)x∈（0，x＜_to_ra（t5）[2]/3）（0/3］，g2（x，5）＞0，從而f3（x）＞g1（x，5）＞0，繼而f2（x）＞0，得到f1（x）在（0/3］內(nèi)單調(diào)上升.

證明f1（x）=-ln（u（x））-1/v（x）*ln（x/sin（x）），由于u（0）=1，v（0）=且當(dāng)x→0＋，ln（x/sin（x））→0，所以當(dāng)x→0＋，f1（x）→0.而由引理3.1，當(dāng)x∈（0，/3］，f1（x）關(guān)于x單調(diào)上升，從而f1（x）＞0.

證明 令w3（x）=nume（rw1（x））*denom（w1（x）），得到

令w4（（x，n）=subs（=_to_ra（tn）[2]，w3＋）＋subs（=_to_ra（tn）[1]，w3-），則w4（x，n）是關(guān)于x 的有理多項(xiàng)式，且對任意n∈N，w4（x，n）＞w3（x）；

使用BOTTEMA 的xprove 指令：xprove（w4（x，n）＜0，[x＜_to_ra（tn）[2]/2]），當(dāng)n=2 時(shí)，w4（x，n）＜0 成立，即在（0/2］內(nèi)0＞w4（x，2）＞w3（x），從而w1（x）＜0.

證明 令f4（x）=-（ln（x/sin（x））＋w2（x）/w1（x）），由引理2.2 知，在（0，/2］內(nèi)w1（x）＜0，所以在（/3，/2］內(nèi)sgn（f4（x））=sgn（f2（x））.

令f5（x）=f4（`x），則f5（x）為包含x、sin（x）、cos（x）、的分式.由于 cos（x）在（/3，/2）內(nèi)不能規(guī)范展開，作變量替換x=/2-y，則f5（x）＜0 在（/3，/2）內(nèi)成立等價(jià)于在（0/6）內(nèi)g（y）=f5（/2-y）＜0 成立.

令g1（y）=numer（g（y））*denom（g（y））；

令g2（y，n）=subs（sin（y）=sin_max（y，n），g1＋）＋subs（sin（y）=sin_min（y，n），g1-），則對任意n∈N，g2（y，n）＞g1（y）；

令g3（y，n）=subs（cos（y）=cos_max（y，n），g2＋）＋subs（cos（y）=cos_min（y，n），g2-），則對任意n∈N，g3（y，n）＞g2（y，n）；

令g4（y，n）=sub（s=_to_ra（tn）[2]，g3＋）＋sub（s=_to_ra（tn）[1]，g3-），則g4（y，n）是關(guān)于y 的一元有理多項(xiàng)式，且g4（y，n）＞g3（y，n）＞g2（y，n）＞g1（y）；

使用BOTTEMA 的xprove 指令：xprove（g4（y，n）＜0，[y＜_to_rat（n）[2]/6]）， 當(dāng)n=8 時(shí)，不等式g4（y，n）＜0 成立，即在（0/6）內(nèi)g1（y）＜0 成立，g（y）＜0 成立.從而在（/3/2）內(nèi)f5（x）＜0 成立.由此得到f4（x）在（/3/2）內(nèi)單調(diào)下降.

下面討論f2（/2）的符號.令

h1=nume（rf2（/2））*denom（f2（/2））=其中和ln（/2）需要有理化，令t=/2-1，則 t∈（0，1），ln（1＋t） 可以規(guī)范展開，即對任意 n∈N，ln_max（t，n）＞ln（1＋t）=ln（/2）＞ln_min（t，n），令 E（n）=subs（t=/2-1，ln_max（t，n）），F(xiàn)（n）=subs（t=/2-1，ln_min（t，n）），則 E（n）＞ln（/2）＞F（n）.

令h2（n）=subs（ln（/2）=E（n），h1＋）＋subs（ln（/2）=F（n），h1-）；

令h3（n）=subs（=_to_ra（tn）[2]，h2（n）＋）＋subs（=_to_ra（tn）[1]，h2（n）-），則對任意n∈N，h3（n）＞h2（n）＞h1.h3（n）是含n 的有理式且容易得到h3（5）＜0，所以h1＜0，從而f2（/2）＜0.

f2（/2）＜0 就得到f4（/2）＜0 成立.又由引理2.1 知f2（/3）＞0，所以f4（/3）＞0，從而在（/3，/2）內(nèi)存在唯一x0使得f4（x0）=0，并且在（/3，x0）內(nèi)f4（x）＞0，從而f2（x）＞0，在（x0，/2）內(nèi)f4（x）＜0，從而f2（x）＜0.

而f2（x）=f1（`x），所以f1（x）在（/3，x0）內(nèi)單調(diào)上升，在（x0/2）內(nèi)單調(diào)下降.由推論2.1 知f1（/3）＞0，從而f1（x）＞0 在（/3，x0]內(nèi)成立；而f1（/2）=0，所以f1（x）＞0 在（x0/2）內(nèi)成立.所以f1（x）＞0 在（/3，/2）內(nèi)成立.

由推論2.1 和引理2.3 知f1（x）＞0 在（0，/2）內(nèi)成立，從而 （fx）＞0 在（0，/2）內(nèi)成立，即定理2 成立.

3 結(jié)束語

逐次Taylor 替換是處理超越函數(shù)多項(xiàng)式不等式自動證明的有效方案，其主要思路是借助Taylor 展開式建立一個(gè)逼近目標(biāo)函數(shù)的多項(xiàng)式套，從而將證明轉(zhuǎn)化為一系列的一元多項(xiàng)式不等式的驗(yàn)證，然后借助BOTTEMA 等代數(shù)不等式證明工具完成最后的工作.算法可以處理含多個(gè)不同超越因子和復(fù)合超越因子的超越函數(shù)多項(xiàng)式不等式，在證明過程中若結(jié)合人工證明和巧妙的代換方法，更能發(fā)揮逐次Taylor 替換算法的效能.

本文解決了一個(gè)一類形如sin（x）/x＞u（x）v(x)的冪指函數(shù)不等式的機(jī)器證明問題，是逐次Taylor 替換成功運(yùn)用的案例.雖然結(jié)論是已知結(jié)果，但方法本身對同類不等式具有示范性，能夠?yàn)槲墨I(xiàn)[1-11]中其它冪指函數(shù)不等式（或冪函數(shù)不等式）的機(jī)器提供證明方案.