陳世平，劉 忠

（1.中國民航飛行學(xué)院德陽校區(qū)四川省商貿(mào)學(xué)校，四川 德陽 618000；2.樂山職業(yè)技術(shù)學(xué)院，四川 樂山 614000）

三角函數(shù)多項(xiàng)式不等式的自動證明

陳世平1，劉 忠2

（1.中國民航飛行學(xué)院德陽校區(qū)四川省商貿(mào)學(xué)校，四川 德陽 618000；2.樂山職業(yè)技術(shù)學(xué)院，四川 樂山 614000）

本文討論了三角函數(shù)多項(xiàng)式特別是正切函數(shù)多項(xiàng)式的性質(zhì)，并在此基礎(chǔ)上實(shí)現(xiàn)了一個三角函數(shù)多項(xiàng)式不等式自動證明的完備算法.算法運(yùn)用Taylor展開式將目標(biāo)不等式的證明轉(zhuǎn)化為一系列的一元多項(xiàng)式不等式的驗(yàn)證，再借助代數(shù)不等式證明工具（如Bottema）完成最后的工作.實(shí)驗(yàn)結(jié)果表明算法對常見的三角函數(shù)多項(xiàng)式不等式十分高效，同時證明過程是“可讀”的.

三角函數(shù)多項(xiàng)式；三角函數(shù)多項(xiàng)式不等式；自動證明；Taylor展開式；終止性

0 引言

不等式的機(jī)器判定問題，一直以來都是數(shù)學(xué)機(jī)械化和自動推理領(lǐng)域研究熱點(diǎn)和難點(diǎn)問題.近年來，代數(shù)不等式的自動證明吸引了大批學(xué)者研究，也取得了巨大的成功，特別是楊路教授提出了降維算法，據(jù)之編制的通用程序BOTTEMA能夠成批驗(yàn)證不等式[1-8]，但BOTTEMA只能處理代數(shù)不等式或先把幾何不等式轉(zhuǎn)化為代數(shù)不等式，尚不能解決一般的超越不等式自動證明問題.關(guān)于超越不等式已有了大量的研究成果和證明方法，但這些成果和方法不能適應(yīng)數(shù)學(xué)機(jī)械化和推理自動化的需要.超越不等式自動證明的困難在于至今其求根問題沒有得到全面解決，不等式的自動證明研究目前還主要基于多項(xiàng)式和代數(shù)函數(shù)，其成果對非多項(xiàng)式以及非代數(shù)函數(shù)不等式都不能直接使用，故有必要對此類不等式的自動證明進(jìn)行研究，探索新的算法.楊路教授也曾指出“BOTTEMA目前尚不適合處理類似sin（x）

針對楊路教授提出的問題，文[4]提出了同一變量不在三角函數(shù)內(nèi)外同時出現(xiàn)即具有模型f（t1（x），t2（x），…，tn（x））>0的不等式的證明方案（其中ti（x）為關(guān)于x的六個基本三角函數(shù)sin（kx）、cos（kx）、tan（kx）、cot（kx）、sec（kx）、csc（kx）形式之一，k為有理數(shù)，f為代數(shù)函數(shù)），并為相同變量在三角函數(shù)內(nèi)外同時出現(xiàn)即具有模型f（x，t1（x），t2（x），…，tn（x））>0的不等式設(shè)計(jì)了一個試探性算法，能夠證明一定難度的三角函數(shù)不等式.文獻(xiàn)[5]以具有模型f（x，tan（x/2））>0的三角函數(shù)不等式為研究對象來探討超越不等式的機(jī)器證明問題，運(yùn)用Taylor展開式建立一個逼近f（x，tan（x/2））的多項(xiàng)式區(qū)間套，從而將證明轉(zhuǎn)化為一系列的一元多項(xiàng)式不等式的驗(yàn)證，然后借助代數(shù)不等式證明工具（如Bottema）完成最后的工作，回避了討論方程根的問題，對常見的三角函數(shù)不等式十分高效.但文獻(xiàn)[5]沒有討論非嚴(yán)格的三角函數(shù)不等式證明問題，也沒有解決算法的終止性問題.

本文的主要目的就是解決文獻(xiàn)[5]中算法的終止性問題，是其工作的延續(xù).首先引入三角函數(shù)多項(xiàng)式以及正切函數(shù)多項(xiàng)式的廣義多項(xiàng)式概念，借助超越數(shù)理論和多項(xiàng)式理論及工具討論了正切函數(shù)多項(xiàng)式的性質(zhì)，并得到了不可約二元有理多項(xiàng)式對應(yīng)的正切函數(shù)多項(xiàng)式在區(qū)間（0，π/2］內(nèi)沒有重根的結(jié)論，進(jìn)而解決了文獻(xiàn)[5]中的非嚴(yán)格不等式證明問題和算法的終止性問題.再把算法擴(kuò)展到可約二元有理多項(xiàng)式對應(yīng)的正切函數(shù)多項(xiàng)式以及更一般的三角函數(shù)多項(xiàng)式，實(shí)現(xiàn)一個三角函數(shù)多項(xiàng)式自動證明的完備算法，解決了楊路教授中提出的“類似sin（x）

1 三角函數(shù)多項(xiàng)式

先給出一些有關(guān)代數(shù)數(shù)和超越數(shù)的基本知識：

定義1.1給定一個復(fù)數(shù)α，若存在某個系數(shù)不全為零的整系數(shù)多項(xiàng)式P（x），使得P（α）=0，則稱α是代數(shù)的或α是代數(shù)數(shù)，否則稱α是超越數(shù).

引理1.1[10]每一個代數(shù)數(shù)系數(shù)多項(xiàng)式的根也是代數(shù)數(shù).

引理1.2[10]若α≠0，則α與tan（α）二者之中至少一個為超越數(shù)；eπ為超越數(shù).

定義1.2設(shè)f（x，x1，…，xn）是n+1元多項(xiàng)式，將變量x1，…，xn用sin（kx）、cos（kx）、tan（kx）（k為任意有理數(shù)）等三角函數(shù)替換后得到的函數(shù)稱為三角函數(shù)多項(xiàng)式；若f是有理多項(xiàng)式，則稱替換后的函數(shù)為有理三角函數(shù)多項(xiàng)式.

給定二元有理系數(shù)多項(xiàng)式環(huán)Q[x，y]，定義該環(huán)上一個映射：hom：f（x，y）→F（x），將變量y用tan（x/2）代替.

定義1.3給定二元有理多項(xiàng)式f（x，y）（0≦x≦π/2，0≦y≦1），它在映射hom下的像F（x）=hom（f）=f（x，tan（x/2））（0≦x≦π/2）稱為正切函數(shù)多項(xiàng)式.

若無歧義，本文F（x）均表示正切函數(shù)多項(xiàng)式f（x，tan（x/2））.特別地，若fy′（x，y）=0，即f（x，y）=F（x）是x的一元多項(xiàng)式；若fx′（x，y）=0，即f（x，y）是y的一元多項(xiàng)式，此時hom（f）是關(guān)于tan（x/2）的多項(xiàng)式，相關(guān)不等式自動證明的討論已在文獻(xiàn)[4]完成.若非特別說明，本文均假定fy′（x，y）≠0，fx′（x，y）≠0.

若非特別說明本文還假定0≦x≦π/2，0≦y≦1.

引理1.3 若有理多項(xiàng)式f（x，y）≠0，則F（x）=hom（f）≠0.

證明假設(shè)f（x，y）≠0，而F（x）=hom（f）=0.將f（x，y）按x降冪排列為qm（y）xm+ qm-1（y）xm-1+…+q0（y），如果m=0，即f（x，y）=q0（y），引理顯然成立，下設(shè)qm（y）不恒等于0且 m>0.由tan（π/4）=1和tan（x）知：當(dāng)自然數(shù)n>1時，tan（π/2n+1）都是代數(shù)數(shù)，記為tn，而F（π/2n）=qm（tn）（π/2n）m+qm-1（tn）（π/2n）m-1+…+q0（tn），每個qi（tn）（i=1，…，m，n=1，2，……）均為代數(shù)數(shù)，π/2n為超越數(shù)，所以如果F（π/2n）=0，則qm（tn）=0，qm-1（tn）=0，…，q0（tn）=0.

即是說方程一元多項(xiàng)式方程qm（y）=0有無數(shù)多個解，此時只能qm（y）恒等于0，與假設(shè)矛盾，即引理成立.

正切函數(shù)多項(xiàng)式（定義域限定在［0，π/2］）具有環(huán)的代數(shù)結(jié)構(gòu)，即hom是二元有理系數(shù)多項(xiàng)式環(huán)到正切函數(shù)多項(xiàng)式環(huán)的一個映射.由引理2.3知映射hom是一一的，顯然也是滿射，所以hom存在逆映射hom-1.

引理1.4 正切函數(shù)多項(xiàng)式F（x）=f（x，tan（x/2））在求導(dǎo)運(yùn)算下封閉，即F′（x）還是正切函數(shù)多項(xiàng)式.

顯然F′（x）=fx′（x，tan（x/2））+（1+tan2（x/2））*fy′（x，tan（x/2））/2.

記f′（x，y）=hom-1（（hom（f））x′），則f′（x，y）=fx′（x，y）+（1+y2）fy′（x，y）/2.

引理1.5 若f（x，y）為不可約二元有理多項(xiàng)式，則f（x，y）與f′（x，y）關(guān)于y的Sylvester結(jié)式resy（f（x，y），f′（x，y））不恒等于0.

證明若resy（f（x，y），f′（x，y））恒等于0，則gcd（f（x，y），f′（x，y））≠1，因f（x，y）不可約，所以f（x，y）|f′（x，y），從而degx（f（x，y））≤degx（f′（x，y））,degy（f（x，y））≤degy（f′（x,y））.而又因?yàn)閒′（x，y）=fx′（x，y）+（1+y2）fy′（x，y）/2，所以degx（f（x，y））≥degx（f′（x，y）），degy（f（x，y））≥degy（f′（x，y））-1，只可能出現(xiàn)兩種情形：

1.degx（f（x，y））=degx（f′（x，y）），degy（f（x，y））=degy（f′（x，y）），即存在常數(shù)c，f′（x，y）= c*f（x，y）;

2.degx（f（x，y））=degx（f′（x，y）），degy（f（x，y））+1=degy（f′（x，y）），即存在常數(shù)c和a，f′（x，y）=c*（y-a）*f（x，y）.

先將f（x，y）按y降冪排列為pn（x）yn+pn-1（x）yn-1+…+p0（x）,由于本文假設(shè)fy′（x，y）≠0，不妨設(shè)pn（x）≠0且n>0.

若出現(xiàn)第1種情形：

得到coeff（f′（x，y），yn+1）=n*pn（x）/2，而coeff（f（x，y），yn+1）=0，推出pn（x）=0，這與已知結(jié)論矛盾.

若出現(xiàn)第2種情形：

論斷 c和a均為有理數(shù)且c=n/2.

證明 coeff（c*（y-a）*f（x，y），yn+1）=c*pn（x），而f′（x，y）=c*（y-a）*f（x，y），所以c*pn（x）=n*pn（x）/2，即c=n/2；因?yàn)槎囗?xiàng)式f（x，y）非0，所以存在有理數(shù)x0和y0，f（x0，y0）≠0，而f（x，y）、f′（x，y）均為有理多項(xiàng)式，所以f（x0，y0）和 f′（x0，y0）為有理數(shù)，f′（x0，y0）=c*（y0-a）*f（x0，y0），即a為有理數(shù). 論斷成立.

再將f（x，y）按x降冪排列為qm（y）xm+qm-1（y）xm-1+…+q0（y），由于本文假設(shè)fx′（x，y）≠0，不妨設(shè)qm（y）≠0且m>0.因?yàn)閒′（x，y）=fx′（x，y）+（1+y2）fy′（x，y）/2=m*qm（y）xm-1+（m-1）*qm-1（y）xm-2+…+q1（y）+（1+y^2）*（qm′（y）xm+qm-1′（y）xm-1+…+q0′（y））/2，所以coeff（f′（x，y），xm）=（1+y^2）*qm′（y）/2；而coeff（c*（y-a）*f（x，y），xm）=c*（y-a）*qm（y），即（1+y^2）*qm′（y）/2=c*（y-a）*qm（y），當(dāng)qm（y）≠0時，解該微分方程得到qm（y）= c0（1+y2）ce(-2acarctan(y))，其中c0為任意常數(shù)（因qm（y）不恒等于0，c0≠0）.

與此同時，qm（y）是y的一元有理多項(xiàng)式，其根最多為有限多個，所以存在δ∈（0，1），當(dāng)y∈（0，δ）時qm（y）≠0，即在定義域（0，δ）內(nèi)，qm（y）=c0（1+y2）ce(-2acarctan(y))，當(dāng)y→0+時，qm（y）的極限為c0，由qm（y）的連續(xù)性得到c0=qm（0）.

同樣的道理，存在δ∈（0，1），當(dāng)y∈（1–δ，1）時qm（y）≠0，即在定義域（1–δ，1）內(nèi)當(dāng)y→1-時，qm（y）的極限qq為其中為代數(shù)數(shù)，eπ為超越數(shù)，為有理數(shù)，所以qq為超越數(shù)，而qm（1）顯然為代數(shù)數(shù)，這與qm（y）的連續(xù)性矛盾.

所以1、2兩種情形都不可能，即resy（f（x，y），f′（x，y））不能恒等于0，引理成立.

定義1.4x0稱為是F（x）的重根，如果F（x0）=F′（x0）=0.

引理1.6 F（x）有重根當(dāng)且僅當(dāng)方程組f（x，y）=0，f′（x，y）=0，y=tan（x/2）有解.

引理1.7 若f（x，y）是不可約有理多項(xiàng)式，則當(dāng)y0=tan（x0/2）和x0（0

證明因?yàn)橛梢?.2知若α≠0，則α與tan（α）二者之中至少一個為超越數(shù)，所以當(dāng)y0是代數(shù)數(shù)時，x0必為超越數(shù)，將f（x，y）按x降冪排列為qm（y）xm+qm-1（y）xm-1+…+q0（y），本文假定fx′（x，y）≠0，所以不妨設(shè)其中m>0且qm（y）不恒等于0，因?yàn)閒（x,y）是不可約,所以qm（y0）、qm-1（y0）、…、q0（y0）是不全為0的代數(shù)數(shù)，由引理2.1知對任意超越數(shù)x，f（x，y0）均不等于0，特別地F（x0）=f（x0，y0）≠0.

同樣的道理，當(dāng)x0是代數(shù)數(shù)時，y0=tan（x0/2）為超越數(shù)，F(xiàn)（x0）≠0.

引理1.8 若f（x，y）為不可約二元有理多項(xiàng)式，F(xiàn)（x）=hom（f），則F（x）在（0，π/2］內(nèi)無重根.

證明令r（x）=resy（f（x，y），f′（x,y）），由引理2.5知r（x）不恒等于0.分兩種情況討論：

（1）r（x）是非0常數(shù)，此時f（x，y）與f′（x，y）沒有公共根，當(dāng)然F（x）與F′（x）也沒公根；

（2）r（x）是關(guān)于x的多項(xiàng)式，設(shè)x0是（0，π/2］內(nèi)F（x）的一個重根，則r（x0）=F（x0）= F′（x0）=0，由r（x0）=0知x0是代數(shù)的.由引理2.7知f（（x0，tan（x0/2））≠0，這與F（x0）=0矛盾，即F（x）沒有重根.

引理1.9 對每個非0正切函數(shù)多項(xiàng)式F（x），存在δ∈（0，π/2），當(dāng)x∈（0，δ）時，F(xiàn)（x）≠0.

證明因?yàn)閠an（x）在0點(diǎn)的taylor展開式T1+T2+T3+…在|x|<π/2時收斂于tan（x），其中為貝努利數(shù)，所以F（x）=f（x，tan（x/2））在0點(diǎn)的taylor展開式在|x|≦π/2時也應(yīng)收斂于F（x），由于F（x）≠0，所以F（x）在0點(diǎn)的各階導(dǎo)數(shù)不能全為0，即存在d≥0，F(xiàn)(d)（0）≠0，不妨設(shè)當(dāng)n=0，1，2，…，（d-1）時F(n)（0）=0.

令H（x）=F（x）/xd，則當(dāng)x→0+時，H（x）=F(d)（0）/d!+o（x）→F(d)（0）/d!，記為c，顯然c≠0.當(dāng)c>0時，存在δ∈（0，π/2），當(dāng)x∈（0，δ）時，H（x）>0，從而F（x）=H（x）*xd>0；當(dāng)c<0時，存在δ∈（0，π/2），當(dāng)x∈（0，δ）時，H（x）<0，從而F（x）=H（x）*xd<0，即引理成立.

引理1.10 若f（x，y）為二元有理多項(xiàng)式，F(xiàn)（x）=hom（f）在［0，π/2］內(nèi)最多有有限個不同的實(shí)根（重根只記一次）.

證明首先假設(shè)f（x，y）不可約.設(shè)F（x）在［0，π/2］有無限個不同的實(shí)根（重根只記一次）.由引理2.9，存在δ∈（0，π/2），當(dāng)x∈（0，δ）時，F(xiàn)（x）≠0，即F（x）在［δ，π/2］內(nèi)有無限個不同的實(shí)根.

令a1=δ，b1=π/2，c1=（a1+b1）/2；

若F（x）在［a1，c1］的實(shí)根有無限個，令a2=a1，b2=c1；

若F（x）在［a1，c1］的實(shí)根只有有限個，則在［c1，b1］內(nèi)必有無限個，令a2=c1，b2=b1；

令c2=（a2+b2）/2；

……；

若F（x）在［an，cn］的實(shí)根有無限個，則令an+1=an，bn+1=cn；

若F（x）在［an，cn］的實(shí)根最多有有限個，則在［cn，bn］內(nèi)必有無限個，令an+1=cn，bn+1=bn；

令cn+1=（an+1+bn+1）/2；……；

若f（x，y）可約，則可以分解為最多有限個不可約多項(xiàng)式的乘積，每個不可約多項(xiàng)式對應(yīng)的正切多項(xiàng)式在［0，π/2］最多有有限個不同的實(shí)根，F(xiàn)（x）在［0，π/2］內(nèi)也最多有有限個不同的實(shí)根.

引理1.11 對（0，π/2）內(nèi)的任意x0，F(xiàn)（x0）=0且在x0的某空心鄰域內(nèi)大于0或小于0，則F′（x0）=0.

定理1.1若f（x，y）為不可約二元有理多項(xiàng)式，F(xiàn)（x）=hom（f），在（0，π/2］內(nèi)不等式F（x）>0與F（x）≧0等價(jià).

證明只需證明在（0，π/2］內(nèi)，若F（x）≧0成立，則F（x）>0成立.

假設(shè)F（x）≧0成立但F（x）>0不成立，即存在x0∈（0，π/2］，F(xiàn)（x0）=0，而由引理2.10，F(xiàn)（x）在［0，π/2］內(nèi)的實(shí)根最多只有有限個，由引理2.7知x0≠π/2，所以存在x0的某空心鄰域，F(xiàn)（x）在其內(nèi)不等于0，即F（x）>0，由引理2.11知F′（x0）=0，即x0是F（x）的重根，與引理2.8矛盾.

推論1.1若f（x，y）為不可約二元有理多項(xiàng)式，F(xiàn)（x）=hom（f），在（0，π/2］上不等式F（x）<0與F（x）≦0等價(jià).

本節(jié)的最后討論可約多項(xiàng)式映射的正切函數(shù)多項(xiàng)式的性質(zhì).

引理1.12 設(shè)f1（x，y）、f2（x，y）是二元有理多項(xiàng)式，F(xiàn)1（x）=hom（f1），F(xiàn)2（x）=hom（f2），則方程F1（x）=0與F2（x）=0有公根的充要條件是方程組f1（x，y）=0，f2（x，y）=0，y=tan（x/2）有解.

定理1.2設(shè)f1（x，y）、f2（x，y）是一對互素的不可約二元有理多項(xiàng)式，F(xiàn)1（x）=hom（f1），F(xiàn)2（x）=hom（f2），則F1（x）與F2（x）沒有非0的公根.

證明 令r（x）=resy（f1（x，y），f2（x，y）），若r（x）=0，因f1、f2均不可約，所以f1（x，y）|f2（x，y）且f2（x，y）|f1（x，y），這與二者互素的條件矛盾，也就是說r（x）不恒等于0.

設(shè)x0是F1（x）與F2（x）的一個公根且x0≠0，則r（x0）=F1（x0）=F2（x0）=0，由r（x0）=0知x0是非0代數(shù)數(shù)，由引理2.7，f1（x0，tan（x0/2））≠0，f2（x0，tan（x0/2））≠0，矛盾.即F1（x）與F2（x）沒有公根.

推論1.2設(shè)二元有理多項(xiàng)式f（x，y）=p（x，y）*P（x，y），其中p（x，y）不可約且與P（x，y）互素，x0是hom（p）在（0，π/2］內(nèi)的實(shí)根，則F（x）=hom（f）在x0的某鄰域內(nèi)在x0兩邊異號.

證明由引理2.8，x0不是hom（p）在（0，π/2］內(nèi)的重根，所以p（x，y）在x0的某鄰域內(nèi)在x0兩邊異號.

p（x，y）不可約且與P（x，y）互素，則p（x，y）不可約且與P（x，y）的每個因式都互素，由定理2.2知道x0不是hom（P）在（0，π/2］內(nèi)的根，又由引理2.10知道，hom（P）在（0，π/2］內(nèi)的實(shí)根最多有限個，即hom（P）在x0的某鄰域內(nèi)無實(shí)根，在該鄰域內(nèi)x0兩邊同號.

所以在上述兩個鄰域的交集內(nèi)，F(xiàn)（x）=hom（f）=hom（p）*hom（P）在x0兩邊異號.

2 三角函數(shù)多項(xiàng)式不等式的自動證明

本節(jié)討論具有模型f（x，tan（x/2））>0（0

用f+和f-分別表示多項(xiàng)式f（x，y）展開式的正項(xiàng)和負(fù)項(xiàng)，顯然f=f++f-，且下面的引理成立：

引理2.1 假設(shè)多項(xiàng)式T1（y）>0，T2（y）>0且T1（y）

為方便，我們將函數(shù)f（x）的在0點(diǎn)的Taylor展開式中的前n項(xiàng)記為taylor（f（x），n），即當(dāng)n為奇數(shù)時taylor（arctan（x），n）=x-x3/3+…+x(2n-1)/（2n-1）（0

引理2.2 當(dāng)0

（1）taylor（arctan（x），2m）

（2）taylor（arctan（x），2m）

taylor（arctan（x），2m-1）>taylor（arctan（x），2m+1）.

定義2.1對任意自然數(shù)n，定義

f（x，y）的上限多項(xiàng)式為

T_max（n，f）=f+（2*taylor（arctan（y），2n-1）），y）+f-（2*taylor（arctan（y），2n），y）；

f（x，y）的下限多項(xiàng)式為

T_min（n，f）=f+（2*taylor（arctan（y），2n）），y）+f-（2*taylor（arctan（y），2n-1），y）.

T_max（n，f）和T_min（n，f）是關(guān)于y的單變量多項(xiàng)式，同時f（2*arctan（y），y）也是關(guān)于y的單變量函數(shù)，不妨記為G（y）（0

引理2.3 任意n∈N,在（0,1］上，函數(shù)T_max（n，f）、T_min（n，f）、G滿足以下性質(zhì)：

（1）T_max（n，f）>G>T_min（n，f）;

（2）T_max（n，f）>T_max（n+1，f），T_min（n，f）

（3）T_max（n，-f）=-T_min（n，f），T_max（n，-f）=-T_min（n，f）；

（4）當(dāng)n→∞時，T_max（n，f）→G，T_min（n，f）→G.

即關(guān)于n，T_max（n，f）嚴(yán)格單調(diào)下降，T_min（n，f）嚴(yán)格單調(diào)上升，并且當(dāng)y∈（0，1］時，有如下關(guān)系：

T_min（1，f）（y）

（T_min（1，f）（y），T_max（1，f）（y））?（T_min（2，f）（y），T_max（2，f）（y））?（T_min（3，f）（y），T_max（3，f）（y））?…………?｛G（y｝）.

由arctan（y）在0點(diǎn)的連續(xù)性知G（y）在0點(diǎn)的右極限存在，令G（0）等于G（y）在0點(diǎn)的右極限，則可將G（y）的定義域擴(kuò)展到閉區(qū)間［0，1］；對任意自然數(shù)n，將taylor（arctan（y），n）在點(diǎn)y=0的值定義為0，則可將T_min（n，f）、T_max（n，f）的定義域擴(kuò)展到［0，1］.

引理2.4 G（0）=T_min（n，f）（0）=T_max（n，f）（0）.

定理2.1[5]設(shè)y0∈（0，1］，則G（y0）<0當(dāng)且僅當(dāng)存在n0，使得T_max（n0，f）（y0）≦0.

推論2.1 不等式G（y）≧0（00（0

推論2.2 不等式G（y）≦0（0

證明G（y）≦0（00（00（0

定理2.2[5]任意y∈（0，1］，G（y）>0成立，當(dāng)且僅當(dāng)存在n0使得對任意y∈（0，1］，T_min（n0，f）（y）≥0.

推論2.3 不等式G（y）>0（0

推論2.4 不等式G（y）<0在區(qū)間（0，1］成立，當(dāng)且僅當(dāng)存在n0使得不等式T_max（n，f）（y）≦0在（0，1］成立.

證明由推論3.3知G（y）<0在區(qū)間（a，b］成立當(dāng)且僅當(dāng)n0使得不等式T_min（n0，-f）（y）≥0，等價(jià)于-T_max（n，f）（y）≥0.

引理2.5 若f（x，y）為不可約二元有理多項(xiàng)式，G（y）=f（2*arctan（y），y），則在（0，1］內(nèi)不等式G（y）>0與G（y）≧0等價(jià)，G（y）<0與G（y）≦0等價(jià).

證明 由定理2.1，在（0，π/2］上，不等式F（x）>0與F（x）≧0等價(jià)，在tan（x/2）=y或x=2*arctan（y）的條件下，F(xiàn)（x）=f（x，y）=G（y），所以當(dāng)y∈（0，1］時，不等式G（y）>0與G（y）≧0等價(jià).

由推論2.1知G（y）<0與G（y）≦0也等價(jià).

在以上討論基礎(chǔ)上，我們設(shè)計(jì)了關(guān)于不等式F（x）=f（x，tan（x/2））>0的算法：

算法2.1 prove_trig_ineq_irreducible

輸入：二元有理多項(xiàng)式f（x，y）；

輸出：1表示F（x）=f（x，tan（x/2））在區(qū)間（0，π/2］內(nèi)恒大于0，-1表示恒小于0，0表示F（x）與0無固定大小關(guān)系；

BEGIN

（1）n←1；

（2）計(jì)算f的上（下）限多項(xiàng)式T_max（n，f）、T_min（n，f）；

?。┤魡巫兞慷囗?xiàng)式不等式T_min（n，f）≧0在（0，1］內(nèi)成立，則不等式F（x）>0成立，return 1，算法結(jié)束；

ⅱ）若單變量多項(xiàng)式不等式T_max（n，f）≦0在（0，1］內(nèi)成立，則不等式F（x）<0不成立，return-1，算法結(jié)束；

ⅲ）若T_max（n，f）>0和T_min（n，f）<0在（0，1］內(nèi)均不成立，則F（x）與0無固定大小關(guān)系，return0，算法結(jié)束；

（3）n←n+1，轉(zhuǎn)（2）.

END.

定理2.3 若f（x，y）為不可約二元有理多項(xiàng)式，則算法3.1必然終止.

證明 若G>0或G<0在區(qū)間（0，1］成立，則由推論3.3和3.4知算法終止；

若G>0和G<0在區(qū)間（0，1］均不恒成立，由引理3.5知G≧0和G≦0也均不成立，所以存在y1、y2∈（0，1］，使得G（y1）<0，G（y2）>0，由推論3.1和3.2知存在n1和n2，使得T_max（n1，f）（y1）≦0，T_min（n2，f）（y2）≧0，則算法在n0=max｛n1，n2｝步循環(huán)必然終止.此時G（y1）T_min（n0，f）（y2）≧T_max（n1，f）（y1）≧0，即G與0在（0，1］內(nèi)無固定大小關(guān)系.

我們再來討論可約多項(xiàng)式所映射得到的正切函數(shù)多項(xiàng)式不等式的自動證明.

由推論2.2可以直接得到如下性質(zhì)：

引理2.6 設(shè)二元有理多項(xiàng)式f（x，y）=p（x，y）*P（x，y），其中p（x，y）不可約且與P（x，y）互素，不等式p（x，tan（x/2））>0和p（x，tan（x/2））<0在（0，π/2］上均不恒成立，則f（x，tan（x/2））>0與f（x，tan（x/2））<0在（0，π/2］上也都不成立.

在算法3.1和引理3.6的基礎(chǔ)上，我們設(shè)計(jì)了針對f（x，y）可約時正切函數(shù)多項(xiàng)式f（x，tan（x/2））的不等式的判定算法：

算法2.2 prove_trig_ineq

輸入：二元有理多項(xiàng)式f（x，y）；

輸出：F（x）=f（x，tan（x/2））在區(qū)間（0，π/2］與0的大小關(guān)系；

（2）p←0，q←0；##其中p表示負(fù)項(xiàng)的個數(shù)，q>0表示不等式非嚴(yán)格.

（3）m←1；

i）若dm為奇數(shù)

若fm（x，y）<0成立，p←p+1;

若fm（x，y）<0和fm（x，y）>0均不成立，則原函數(shù)與0的各種不等關(guān)系均不成立，算法結(jié)束.

若dm為偶數(shù)

若fm（x，y）<0和fm（x，y）>0均不成立，q←q+1.

ii）m←m+1若m>n轉(zhuǎn)（4），否則轉(zhuǎn)（i）.

（4）i）若C>0，p為偶數(shù)，q=0，則不等式f>0成立；

ii）若C>0，p為偶數(shù)，q>0，則不等式f≧0成立；

iii）若C>0，p為奇數(shù)，q=0，則不等式f<0成立；

iv）若C>0，p為奇數(shù)，q>0，則不等式f≦0成立；

當(dāng)C<0也可得到相應(yīng)的結(jié)論.

（5）算法結(jié)束.

3 應(yīng)用實(shí)例

f（x，sin（x），cos（x））>0（其中f（x，y，z）是三元多項(xiàng)式且00型不等式，在轉(zhuǎn)化過程中可能會出現(xiàn)分母，即f（x，tan（x/2））是分式，此時可通分后將其分子分母相乘從而得到一個正切函數(shù)多項(xiàng)式.三角函數(shù)不等式中還有一類含tan（x）的不等式十分常見，其定義域往往為（0，π/2），這與算法3.1定理3.3的要求不符，需要做一些處理：

引理3.1[5]設(shè)f（x，y，z，t）是四元多項(xiàng)式，y的最高次數(shù)為n，三角函數(shù)多項(xiàng)式f（x，tan（x），sin（x），cos（x））（00（00（0

引理4.1 將算法3.1和3.2的適應(yīng)范圍擴(kuò)展到模型f（x，tan（x），sin（x），cos（x））>0，當(dāng)然算法還可擴(kuò)展到含有cot（x）、sec（x）、csc（x）等三角函數(shù)的不等式.

在本文的討論中，我們將F（x）=f（x，tan（x/2））的定義域限定在（0，π/2］是因?yàn)閍rctan（y）的 taylor展開式在|y|≦1時收斂.針對更一般的有理三角函數(shù)多項(xiàng)式f（x，tan（k1x），sin（k2x），cos（k3x））（其中k1、k2、k3為有理數(shù)），根據(jù)文獻(xiàn)[13、15]知函數(shù)f可以“歸一”到f（x，tan（k0x））模型（其中k0為有理數(shù)），此時對函數(shù)的定義域要求是k0x∈（0,π/4］.

判斷單變量多項(xiàng)式不等式有很多成熟快捷的算法，如BOTTEMA[6]，文獻(xiàn)[15]以DISCOVER[7]為基礎(chǔ)設(shè)計(jì)一個單變量多項(xiàng)式不等式的判斷算法，也十分高效.

我們用Maple實(shí)現(xiàn)了算法3.1和3.2，下面舉例來描述算法運(yùn)行過程或結(jié)果：

例1 Huygens不等式：（k+1）x

（1）2x

不等式等價(jià)于0

所以原不等式等價(jià)于f（x，y）=2xy4+4y-2x>0（0

（2）3x

不等式等價(jià)于0

所以原不等式等價(jià)于f（x，y）=3xy4-2y3+6y-3x>0（00和-2y3+6y5-2y7<0均不成立；

當(dāng)00顯然成立；

（3）4x

不等式等價(jià)于0

原不等式等價(jià)于f（x，y）=4xy4-4y3+8y-4x>0（0

所以F（x）=sin（x）＋3sin（x）cos（x）－4xcos（x）和0在（0，π/2］內(nèi)無固定大小關(guān)系，即F（x）>0和F（x）<0均不成立，原不等式及其反向不等式均不成立.

不等式可等價(jià)轉(zhuǎn)化為cos（x）sin（x）2+xsin（x）-2x2cos（x）

當(dāng)c=9/45，算法3.1在循環(huán)次數(shù)n=8時終止，不等式成立；

當(dāng)c=8/45，算法3.1在循環(huán)次數(shù)n=19時終止，不等式成立；

當(dāng)c=7/45，算法3.1在循環(huán)次數(shù)n=28時終止，不等式反向成立；

當(dāng)c=6/45，算法3.1在循環(huán)次數(shù)n=8時終止，不等式反向成立.

例3 為描述算法3.2的運(yùn)行過程，我們隨機(jī)產(chǎn)生一個三角函數(shù)多項(xiàng)式：

根據(jù)文獻(xiàn)[12]中的算法，F(xiàn)（x）中的三角函數(shù)可“歸一”到tan（x/2），再去掉恒大于0的分母得到一個有理正切函數(shù)多項(xiàng)式F（x）=x*tan6（x/2）-4x2tan5（x/2）-6tan5（x/2）+4tan6（x/2）x3+29x*tan4（x/2）-12tan3（x/2）-40x2tan3（x/2）+12tan2（x/2）x3+31x*tan2（x/2）-12x2tan（x/2）-6tan（x/2）+3x，F(xiàn)（x）的正負(fù)性等價(jià)于多項(xiàng)式的正負(fù)（其中0

為量化算法3.1的效率，將其證明不等式f>g終止時循環(huán)步數(shù)記為n（f-g）或n（f>g），更多一些例子（定義域均限制在（0，π/2］的運(yùn)行結(jié)果如下：

實(shí)驗(yàn)表明算法3.1和3.2對模型f（x，tan（x），sin（x），cos（x））>0的有理三角函數(shù)多項(xiàng)式不等式（如文獻(xiàn)[11]第五章中的不等式）十分高效，并且可以輸出能夠理解的證明過程.

4 總結(jié)

本文引人三角函數(shù)多項(xiàng)式以及正切函數(shù)多項(xiàng)式的廣義多項(xiàng)式概念，研究其性質(zhì)得到了若f（x，y）為不可約二元有理多項(xiàng)式，對應(yīng)的正切函數(shù)多項(xiàng)式f（x，tan（x/2））在（0，π/2］內(nèi)無重根，從而不等式f（x，tan（x/2））>0與f（x，tan（x/2））≧0等價(jià)的結(jié)論.在此基礎(chǔ)上，實(shí)現(xiàn)了一個三角函數(shù)多項(xiàng)式不等式自動證明的完備算法，在證明不等式過程中運(yùn)用Taylor展開式建立一個逼近f（x，tan（x/2））的多項(xiàng)式區(qū)間套，將證明轉(zhuǎn)化為一系列一元多項(xiàng)式不等式的驗(yàn)證，然后借助代數(shù)不等式證明工具完成最后的工作，回避了不等式證明往往需要的方程根的討論問題.算法簡單易行，十分高效，能夠判斷目標(biāo)函數(shù)在（0，π/2］內(nèi)和0的大小關(guān)系，并且能夠輸出可以理解的證明過程，是不等式的一種“可讀證明”，從而解決了楊路教授在文獻(xiàn)[8]中提出的“類似sin（x）

在本文的討論中，要求多項(xiàng)式的系數(shù)為有理數(shù)是因?yàn)槿呛瘮?shù)多項(xiàng)式的某些性質(zhì)（如引理2.8、定理2.1）在滿足該條件才成立，將F（x）=f（x，tan（x/2））的定義域限定在（0，π/2］是因?yàn)閍rctan（y）的taylor展開式在|y|≦1時收斂，當(dāng)然一個自然的想法是作類似x=t+kπ的變量替換將F（x）=f（x，tan（x/2））的定義域擴(kuò)大，但替換后多項(xiàng)式可能會出現(xiàn)超越數(shù)系數(shù)，從而關(guān)于有理三角函數(shù)多項(xiàng)式的性質(zhì)不再成立，算法也就可能不再適用，至少不再具有完備性，怎么將函數(shù)的定義域擴(kuò)招到整個實(shí)數(shù)域還是值得進(jìn)一步研究的課題.實(shí)驗(yàn)表明，針對一些非有理系數(shù)或定義域超過（0，π/2］的三角函數(shù)多項(xiàng)式不等式，算法3.1也適用，但本文還不能從理論上保證算法必然終止，即算法3.1針對定義域?yàn)椋?，π/2］的有理系數(shù)三角函數(shù)多項(xiàng)式不等式為完備算法，而針對非有理系數(shù)或定義域超過（0，π/2］的三角函數(shù)多項(xiàng)式不等式還只能算作一個試探性算法.

［1］Buchberger B,Collins G E.Algebraic method for geometric reasoning[J].Annual Review of Computer Science,1988,3：85-119.

［2］Wu W T.Basic principles of mechanical theorem proving in elementary geometries[J].Journal of Automated Reasoning，1986，2（3）：221-252.

［3］Yang L,Zhang J.A practical program of automated proving for a class of geometric inequalities[M]// Automated Deduction in Geometry.Berlin:Springer Verlag，2001：41-47.

［4］陳世平.三角函數(shù)不等式的自動證明[J].四川大學(xué)學(xué)報(bào)：自然科學(xué)版，2013，50（3）：537-540.

［5］陳世平，劉忠.Taylor展開式與三角函數(shù)不等式的自動證明[J].系統(tǒng)科學(xué)與數(shù)學(xué)，已錄用.

［6］楊路，夏時洪.一類構(gòu)造性幾何不等式的機(jī)器證明[J].計(jì)算機(jī)學(xué)報(bào)，2003，26（7）：769-778.

［7］楊路，夏壁燦.不等式機(jī)器證明與自動發(fā)現(xiàn)[M].北京：科學(xué)出版社，2008.

［8］楊路，郁文生.常用基本不等式的機(jī)器證明[J].智能系統(tǒng)學(xué)報(bào)，2011，6（5）：377-390.

［9］徐鳴.程序驗(yàn)證與系統(tǒng)分析的若干符號計(jì)算問題[D].上海：華東師范大學(xué)，2010.

［10］Parshin A N,Shafarevivh I R.數(shù)論4：超越數(shù)[M].北京：科學(xué)出版社，2009.

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

［12］陳世平，張景中.初等不等式的可讀證明的自動生成[J].四川大學(xué)學(xué)報(bào)：工程科學(xué)版，2003，35（4）：86-93.

［13］陳世平，張景中.三角不等式的自動證明[J].四川大學(xué)學(xué)報(bào)：自然科學(xué)版，2003，40（4）：686-690.

［14］徐嘉，姚勇.一類根式不等式的有理化算法與機(jī)器證明[J].計(jì)算機(jī)學(xué)報(bào)，2008，31（2）：24-31.

［15］陳世平，劉忠.一類三角形幾何不等式的自動證明[J].計(jì)算機(jī)應(yīng)用研究,2012，29（5）：1732-1736.

［16］陳世平.由初等數(shù)學(xué)實(shí)現(xiàn)三角形幾何不等式的自動證明[M].中國初等數(shù)學(xué)研究，2011（3）：24.

［17］姚勇.基于列隨機(jī)矩陣的逐次差分代換與正半定型的機(jī)械化判定[J].中國科學(xué)：數(shù)學(xué)，2010，40（3）：251-264.

［18］楊路,姚勇.差分代換矩陣與多項(xiàng)式的非負(fù)性判定[J].系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（9）：1169-1177.

［19］Zhu L.Some new wilker type inequalities for circular and hyperbolic functions[J/OL].Abstract and Applied Analysis,2009[2015-01-12].http://dx.doi.org/10.1155/2009/485842.

Automated Proving of Trigonometric Function Polynomial Inequalities

Chen Shiping1,Liu Zhong2
（1.Deyang Branch，University of China Civil Aviation Flight and Sichuan Trade School,Deyang 618000,Sichuan，China, 2.Leshan Vocation and Technology College，Leshan 614000，Sichuan，China）

The property of the trigonometric function polynomial，especially tangent function polynomial is discussed.A complete algorithm proving the trigonometric function polynomial inequalitiesmechanicallyispresented.ThroughTaylorexpansion，theproofofthetargetinequality is transformed to the verification of a series of polynomial inequalities with only one variable,and then completed by algebraic inequality-proving package such as BOTTEMA.Experiments show that the algorithm is very effective for common trigonometric function polynomial inequalities,and theprocedureis“readable”.

trigonometric function polynomial；trigonometric function polynomial inequality；mechanical proving；Taylor expansion；termination

TP181

A

1001-4217（2015）03-0043-130

2015-01-15

陳世平，（1970－），男，博士，高級講師，研究方向：機(jī)器證明、符號計(jì)算等領(lǐng)域研究. E-mail:chinshiping@sina.com.