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

陳世平，劉 忠

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

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

陳世平1，劉 忠2

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

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

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

0 引言

不等式的機器判定問題，一直以來都是數(shù)學(xué)機械化和自動推理領(lǐng)域研究熱點和難點問題.近年來，代數(shù)不等式的自動證明吸引了大批學(xué)者研究，也取得了巨大的成功，特別是楊路教授提出了降維算法，據(jù)之編制的通用程序BOTTEMA能夠成批驗證不等式[1-8]，但BOTTEMA只能處理代數(shù)不等式或先把幾何不等式轉(zhuǎn)化為代數(shù)不等式，尚不能解決一般的超越不等式自動證明問題.關(guān)于超越不等式已有了大量的研究成果和證明方法，但這些成果和方法不能適應(yīng)數(shù)學(xué)機械化和推理自動化的需要.超越不等式自動證明的困難在于至今其求根問題沒有得到全面解決，不等式的自動證明研究目前還主要基于多項式和代數(shù)函數(shù)，其成果對非多項式以及非代數(shù)函數(shù)不等式都不能直接使用，故有必要對此類不等式的自動證明進行研究，探索新的算法.楊路教授也曾指出“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è)計了一個試探性算法，能夠證明一定難度的三角函數(shù)不等式.文獻[5]以具有模型f（x，tan（x/2））>0的三角函數(shù)不等式為研究對象來探討超越不等式的機器證明問題，運用Taylor展開式建立一個逼近f（x，tan（x/2））的多項式區(qū)間套，從而將證明轉(zhuǎn)化為一系列的一元多項式不等式的驗證，然后借助代數(shù)不等式證明工具（如Bottema）完成最后的工作，回避了討論方程根的問題，對常見的三角函數(shù)不等式十分高效.但文獻[5]沒有討論非嚴格的三角函數(shù)不等式證明問題，也沒有解決算法的終止性問題.

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

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

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

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

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

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

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

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

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

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

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

引理1.3 若有理多項式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.

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

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

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

顯然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）為不可約二元有理多項式，則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））.而又因為f′（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；因為多項式f（x，y）非0，所以存在有理數(shù)x0和y0，f（x0，y0）≠0，而f（x，y）、f′（x，y）均為有理多項式，所以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.因為f′（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的一元有理多項式，其根最多為有限多個，所以存在δ∈（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）是不可約有理多項式，則當(dāng)y0=tan（x0/2）和x0（0

證明因為由引理2.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，因為f（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）為不可約二元有理多項式，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的多項式，設(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ù)多項式F（x），存在δ∈（0，π/2），當(dāng)x∈（0，δ）時，F(xiàn)（x）≠0.

證明因為tan（x）在0點的taylor展開式T1+T2+T3+…在|x|<π/2時收斂于tan（x），其中為貝努利數(shù)，所以F（x）=f（x，tan（x/2））在0點的taylor展開式在|x|≦π/2時也應(yīng)收斂于F（x），由于F（x）≠0，所以F（x）在0點的各階導(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）為二元有理多項式，F(xiàn)（x）=hom（f）在［0，π/2］內(nèi)最多有有限個不同的實根（重根只記一次）.

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

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

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

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

令c2=（a2+b2）/2；

……；

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

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

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

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

引理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）為不可約二元有理多項式，F(xiàn)（x）=hom（f），在（0，π/2］內(nèi)不等式F（x）>0與F（x）≧0等價.

證明只需證明在（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)的實根最多只有有限個，由引理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）為不可約二元有理多項式，F(xiàn)（x）=hom（f），在（0，π/2］上不等式F（x）<0與F（x）≦0等價.

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

引理1.12 設(shè)f1（x，y）、f2（x，y）是二元有理多項式，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）是一對互素的不可約二元有理多項式，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è)二元有理多項式f（x，y）=p（x，y）*P（x，y），其中p（x，y）不可約且與P（x，y）互素，x0是hom（p）在（0，π/2］內(nèi)的實根，則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)的實根最多有限個，即hom（P）在x0的某鄰域內(nèi)無實根，在該鄰域內(nèi)x0兩邊同號.

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

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

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

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

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

為方便，我們將函數(shù)f（x）的在0點的Taylor展開式中的前n項記為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）的上限多項式為

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

f（x，y）的下限多項式為

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的單變量多項式，同時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）嚴格單調(diào)下降，T_min（n，f）嚴格單調(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點的連續(xù)性知G（y）在0點的右極限存在，令G（0）等于G（y）在0點的右極限，則可將G（y）的定義域擴展到閉區(qū)間［0，1］；對任意自然數(shù)n，將taylor（arctan（y），n）在點y=0的值定義為0，則可將T_min（n，f）、T_max（n，f）的定義域擴展到［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，等價于-T_max（n，f）（y）≥0.

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

證明 由定理2.1，在（0，π/2］上，不等式F（x）>0與F（x）≧0等價，在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等價.

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

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

算法2.1 prove_trig_ineq_irreducible

輸入：二元有理多項式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）計算f的上（下）限多項式T_max（n，f）、T_min（n，f）；

ⅰ）若單變量多項式不等式T_min（n，f）≧0在（0，1］內(nèi)成立，則不等式F（x）>0成立，return 1，算法結(jié)束；

ⅱ）若單變量多項式不等式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）為不可約二元有理多項式，則算法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)系.

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

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

引理2.6 設(shè)二元有理多項式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è)計了針對f（x，y）可約時正切函數(shù)多項式f（x，tan（x/2））的不等式的判定算法：

算法2.2 prove_trig_ineq

輸入：二元有理多項式f（x，y）；

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

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

（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)用實例

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

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

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

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

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

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

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

（1）2x

不等式等價于0

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

（2）3x

不等式等價于0

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

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

（3）4x

不等式等價于0

原不等式等價于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均不成立，原不等式及其反向不等式均不成立.

不等式可等價轉(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的運行過程，我們隨機產(chǎn)生一個三角函數(shù)多項式：

根據(jù)文獻[12]中的算法，F(xiàn)（x）中的三角函數(shù)可“歸一”到tan（x/2），再去掉恒大于0的分母得到一個有理正切函數(shù)多項式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）的正負性等價于多項式的正負（其中0

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

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

4 總結(jié)

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

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

［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é)報：自然科學(xué)版，2013，50（3）：537-540.

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

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

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

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

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

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

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

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

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

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

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

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

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

［18］楊路,姚勇.差分代換矩陣與多項式的非負性判定[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－），男，博士，高級講師，研究方向：機器證明、符號計算等領(lǐng)域研究. E-mail:chinshiping@sina.com.