單變?cè)呛瘮?shù)不等式的發(fā)現(xiàn)與自動(dòng)證明

何燈，李云杰

（福清第三中學(xué)，福建福清350315）

單變?cè)呛瘮?shù)不等式的發(fā)現(xiàn)與自動(dòng)證明

何燈，李云杰

（福清第三中學(xué)，福建福清350315）

借助于級(jí)數(shù)理論和maple數(shù)學(xué)軟件，本文研究單變?cè)呛瘮?shù)不等式的發(fā)現(xiàn)及機(jī)器自動(dòng)證明，根據(jù)算法所編寫(xiě)的程序hdtrig2015能夠在極短的時(shí)間內(nèi)實(shí)現(xiàn)三角函數(shù)不等式的自動(dòng)驗(yàn)證.豐富的實(shí)例表明本文的算法具有極大的優(yōu)越性，能夠成批實(shí)現(xiàn)三角函數(shù)不等式的機(jī)器自動(dòng)驗(yàn)證.

三角函數(shù)；不等式；泰勒展開(kāi)；機(jī)器證明；實(shí)根隔離

0　引言

不等式的發(fā)現(xiàn)與機(jī)器證明，一直是數(shù)學(xué)機(jī)械化、自動(dòng)推理及智能系統(tǒng)領(lǐng)域的研究難點(diǎn)和熱點(diǎn)問(wèn)題，近年來(lái)得到了長(zhǎng)足的發(fā)展[1-17].特別是楊路教授提出了降維算法[2-3，9，14]，據(jù)之編寫(xiě)的通用程序BOTTEMA能夠成批驗(yàn)證和發(fā)現(xiàn)不等式.BOTTEMA的開(kāi)發(fā)極大地影響著不等式研究者的研究方式和研究方法，但B0TTEMA只能處理代數(shù)不等式或先把幾何不等式轉(zhuǎn)化為代數(shù)不等式，尚不能解決一般的超越不等式自動(dòng)證明問(wèn)題，楊路教授也曾指出：B0TTEMA目前尚不適合處理類(lèi)似sinx＜x＜tanx（0＜x＜/2）這樣的超越不等式，這是值得進(jìn)一步研究的課題[14].

三角函數(shù)不等式的證明是初等不等式證明問(wèn)題的難點(diǎn)，因?yàn)椴粌H要運(yùn)用代數(shù)不等式的方法，而且要使用三角函數(shù)的許多性質(zhì)，如正余弦函數(shù)的有界性、三角函數(shù)的單調(diào)性等，各種三角函數(shù)之間的變換在證明不等式過(guò)程中的目的性、規(guī)律性不強(qiáng)，還有一些特殊方法不易機(jī)械化[5]，受這種種因素的限制，三角函數(shù)不等式的自動(dòng)證明研究一直進(jìn)展緩慢.

文獻(xiàn)[16]中基于區(qū)間分析算法的InequalityProve程序能夠?qū)崿F(xiàn)一些三角函數(shù)不等式的自動(dòng)驗(yàn)證，可是針對(duì)性不強(qiáng)，適用范圍并不廣泛（InequalityProve驗(yàn)證本文例9的問(wèn)題，需借助手動(dòng)分析而無(wú)法實(shí)現(xiàn)完全的機(jī)械式自動(dòng)推理）.

文獻(xiàn)[17]中基于萬(wàn)能代換及級(jí)數(shù)理論的算法能夠解決較大范圍的問(wèn)題，但對(duì)一些較復(fù)雜的不等式，代換后的結(jié)果將極其復(fù)雜，從而給自動(dòng)驗(yàn)證增加了一定的難度，也在一定程度上降低了效率.

本文繼續(xù)探討單變?cè)呛瘮?shù)不等式的發(fā)現(xiàn)及機(jī)器自動(dòng)證明，提出了基于級(jí)數(shù)理論及待定系數(shù)法的三角函數(shù)不等式的自動(dòng)發(fā)現(xiàn)算法，基于級(jí)數(shù)理論及多項(xiàng)式實(shí)根隔離的三角函數(shù)不等式自動(dòng)驗(yàn)證算法，并由此編寫(xiě)了自動(dòng)驗(yàn)證程序hdtrig2015，例舉了豐富的實(shí)例進(jìn)行了程序測(cè)試，這些例子充分體現(xiàn)出本文的算法具有極大的優(yōu)越性，能夠成批實(shí)現(xiàn)三角函數(shù)不等式的機(jī)器自動(dòng)驗(yàn)證，且驗(yàn)證過(guò)程簡(jiǎn)單易懂，是“可讀”的.

1　三角函數(shù)不等式的發(fā)現(xiàn)—模型法

本章節(jié)介紹在maple平臺(tái)上，借助于待定系數(shù)法和三角函數(shù)的泰勒展開(kāi)式，實(shí)現(xiàn)三角函數(shù)不等式發(fā)現(xiàn)的一個(gè)算法.

步驟一（泰勒展開(kāi)）：在maple中執(zhí)行泰勒展開(kāi)式命令taylor（F1，x=0，10），可得以a，b，c，d，e，f為系數(shù)的展開(kāi)式A0+A1x2+A2x4+A3x6+A4x8+O（x9）.

步驟二（解方程組）：在maple中執(zhí)行解方程組命令

步驟三（賦值化簡(jiǎn)）：將方程組的解代入F1中并化簡(jiǎn)，得

步驟四（預(yù)判）：在maple中執(zhí)行畫(huà)圖命令plot（F1，x=0..Pi/2），觀察圖象，可猜測(cè)的上界.

從而猜測(cè)如下雙邊不等式成立（證明見(jiàn)文獻(xiàn)[19]）

依據(jù)上述步驟，可編寫(xiě)maple程序，實(shí)現(xiàn)此類(lèi)三角函數(shù)不等式的自動(dòng)發(fā)現(xiàn).

2　三角函數(shù)不等式的自動(dòng)證明

2.1引理及證明

證明記Si（x）=sin x-s2i+1（x）=sin x-，下面利用數(shù)學(xué)歸納法證明Si（x）≥0.

當(dāng)i=0時(shí)，S0（x）=sinx-s1（x）=sinx-注意到

設(shè)i=l（l∈N+）時(shí)，

綜上，對(duì)任意i∈N，Si（x）=sinx-s2i+1（x）≥0.同理，可證s2i（x）-sinx≥0成立.

由sinx≥s2i+1（x）可得

2.2第一類(lèi)型不等式的驗(yàn)證

在maple中執(zhí)行求導(dǎo)命令FF:=diff（15*F2，x）及去分母命令numer（FF），轉(zhuǎn)化為證明

步驟二（積化和差）：將待證式子積化和差（maple中的命令combine可實(shí)現(xiàn)三角函數(shù)的積化和差），等價(jià)于證明F3＞0，其中

步驟三（縮小為多項(xiàng)式）：借助于泰勒展開(kāi)式和引理，將F3縮小為F4，其中

注1將待證式積化和差，轉(zhuǎn)化為形如F3的形式，使得泰勒展開(kāi)后的式子在保證高精度的情況下能夠達(dá)到最大限度的簡(jiǎn)化.

注2在利用引理對(duì)F3進(jìn)行放縮時(shí)，可取定i為一個(gè)較大的自然數(shù)（如i=3），以避免i從0開(kāi)始逐個(gè)循環(huán)，從而能減少循環(huán)次數(shù)，縮短程序運(yùn)行時(shí)間.

步驟四（系數(shù)有理化）：由于步驟五中的實(shí)根隔離命令realroot要求多項(xiàng)式的系數(shù)必須為有理數(shù)，當(dāng)步驟三中所得多項(xiàng)式的系數(shù)出現(xiàn)無(wú)理數(shù)（含根號(hào)或等，maple中的命令whattype命令檢驗(yàn)系數(shù)是否為整數(shù)、分?jǐn)?shù)，是否含根號(hào)、等）時(shí)，需對(duì)這些無(wú)理系數(shù)進(jìn)行放縮.設(shè)某項(xiàng)的無(wú)理系數(shù)為λ，實(shí)際編程中可取λ的不足近似值其中[x]表示不超過(guò)x的最大整數(shù)，由0≤x-［x］＜1可得來(lái)替代λ以達(dá)到縮小（有理化）的目的，取λ的過(guò)剩近似（同樣由0≤x-［x］＜1可得來(lái)替代λ以達(dá)到放大（有理化）的目的.設(shè)經(jīng)過(guò)系數(shù)有理化處理后，最終所得有理系數(shù)多項(xiàng)式為F5.

注3此例中F4的系數(shù)均為有理數(shù)，經(jīng)步驟四處理以后，所得的多項(xiàng)式F5＝F4.

步驟五（實(shí)根隔離）：借助于maple中的實(shí)根隔離命令realroot（隔離精度為萬(wàn)分之一），得到F5的實(shí)根區(qū)間為

經(jīng)第四步處理后，得F5=F4，經(jīng)第五步求得F5的實(shí)根隔離區(qū)間為

注5為了避免出現(xiàn)死循環(huán)，可限定循環(huán)的次數(shù)以及循環(huán)的時(shí)間，以使得程序能在規(guī)定的次數(shù)或規(guī)定的時(shí)間內(nèi)結(jié)束運(yùn)行.

注6以上六個(gè)步驟適用第一類(lèi)中以x=0為取等條件的情形（因?yàn)椴襟E三中默認(rèn)正余弦函數(shù)在x=0處進(jìn)行泰勒展開(kāi)），當(dāng)需驗(yàn)證以x=/2為取等條件的不等式時(shí)，可作代換x=/2-x，將待證不等式轉(zhuǎn)化為以x=0為取等條件的情形進(jìn)行求證.

2.3第二類(lèi)型不等式的驗(yàn)證

2.2中的算法適用于單個(gè)區(qū)間端點(diǎn)為取等條件的情形，若待證不等式為第二類(lèi)型不等式時(shí)（區(qū)間的兩端點(diǎn)均可取等），則可將區(qū)間分為兩個(gè)小區(qū)間（0，0.8），（/2-0.8，/2），（顯然兩區(qū)間的并區(qū)間為（0，/2））.當(dāng)x∈（0，0.8）時(shí)，此時(shí)待證不等式為第一類(lèi)型不等式（x=0為取等條件），可類(lèi)似于2.2中的步驟驗(yàn)證之.當(dāng)x∈（/2-0.8，π/2），此時(shí)待證不等式為第一類(lèi)型不等式（x=/2為取等條件），可作代換x=/2-x，將待證不等式轉(zhuǎn)化為x=0為取等條件的情形進(jìn)行求解.

2.4hdtrig2015程序模塊介紹

依據(jù)上述算法分析，筆者編寫(xiě)了自動(dòng)驗(yàn)證程序hdtrig2015，該程序由tlsin、tlcos、jinsi、dxssx、geli、hprove這六個(gè)模塊構(gòu)成.

tlsin及tlcos模塊利用了2.1的引理，可實(shí)現(xiàn)正余弦函數(shù)的放縮（2.2步驟三）.

jinsi模塊可實(shí)現(xiàn)無(wú)理系數(shù)的放縮（2.2步驟四）.

dxssx模塊包含了tlsin、tlcos、jinsi三個(gè)模塊，可實(shí)現(xiàn)將一個(gè)三角函數(shù)式縮小為一個(gè)有理系數(shù)多項(xiàng)式（2.2步驟三和步驟四）.

geli模塊可實(shí)現(xiàn)一個(gè)有理系數(shù)多項(xiàng)式的實(shí)根隔離，并判定實(shí)根區(qū)間是否在給定的區(qū)間內(nèi)（2.2步驟五和步驟六）

hprove模塊是程序的主要模塊，包含了dxssx、geli兩個(gè)模塊，綜合實(shí)現(xiàn)了2.2中的六個(gè)步驟.

3　hdtrig2015程序運(yùn)行實(shí)例

在maple15平臺(tái)上，筆者利用hdtrig2015驗(yàn)證了Jordan不等式、Huygens不等式、Wilker不等式、Kober不等式等經(jīng)典三角函數(shù)不等式及其改進(jìn)，下面是一些有代表性的例子.所用計(jì)算機(jī)硬件環(huán)境為Intel（R）Core（TM）i3-2310MCPU@2.10 GHz.

3.1第一類(lèi)型的例子

證明該左邊不等式耗時(shí)0.483 s，進(jìn)行了一次循環(huán).證明右邊不等式耗時(shí)0.436 s，進(jìn)行了一次循環(huán).

例2[18]設(shè)x∈（0，/2），則

證明該左邊不等式耗時(shí)0.764 s，進(jìn)行了一次循環(huán).證明右邊不等式耗時(shí)0.297 s，進(jìn)行了一次循環(huán).

例3[20]設(shè)x∈（0，/2），則，對(duì)G3（x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時(shí)0.967 s，進(jìn)行了一次循環(huán).

例4[19]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)1.326 s，進(jìn)行了兩次循環(huán).例5[21]339（Huygens不等式）設(shè)x∈（0，/2），則2sinx+tanx＞3x.證明該不等式耗時(shí)0.432 s，進(jìn)行了一次循環(huán).

例6[22]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)0.967 s，進(jìn)行了一次循環(huán).

例7[22]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)1.045 s，進(jìn)行了一次循環(huán).

例8[21]339（Wilker不等式）設(shè)x∈（0，/2），則

證明該不等式耗時(shí)0.437s，進(jìn)行了一次循環(huán).

例9[23]設(shè)x∈（0，/2），則記對(duì)G9（x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時(shí)0.967 s，進(jìn)行了兩次循環(huán).

例10[22]設(shè)x∈（0，/2），則記G10（x對(duì)G1（0x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時(shí)0.936 s，進(jìn)行了一次循環(huán).

例11[22]設(shè)x∈（0，/2），則

記G11（x），對(duì)G11（x）求導(dǎo)，去分母，轉(zhuǎn)化為證明

證明該不等式耗時(shí)1.076 s，進(jìn)行了一次循環(huán).

例12[24]（Wilker型不等式）設(shè)x∈（0，/2），則

證明該不等式耗時(shí)0.702 s，進(jìn)行了一次循環(huán).

例13[25]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)0.640 s，進(jìn)行了一次循環(huán).

例14[22]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)0.281 s，進(jìn)行了一次循環(huán).

例15[22]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)0.999 s，進(jìn)行了一次循環(huán).

3.2第二類(lèi)型的例子

例16[20]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)（0.780+0.967）s，各進(jìn)行了一次循環(huán).

例17[19]設(shè)x∈（0，/2），則

證明該不等式耗時(shí)（0.967+1.248）s，各進(jìn)行了一次循環(huán).

例18[26]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.608+0.609）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.296+0.281）s，各進(jìn)行了一次循環(huán).

例19[27]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.655+0.593）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.249+0.343）s，各進(jìn)行了一次循環(huán).

例20[28]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.624+0.566）s，各進(jìn)行了一次循環(huán).右端不等式證明見(jiàn)例19.

例21[28]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.640+0.670）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.281+0.452）s，各進(jìn)行了一次循環(huán).

例22[30]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.655+0.671）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.281+0.468）s，各進(jìn)行了一次循環(huán).

例23[30]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.671+0.671）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.328+0.406）s，各進(jìn)行了一次循環(huán).

例24[31]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.656+1.138）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.484+0.406）s，各進(jìn)行了一次循環(huán).

例25[31]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.967+1.217）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.546+0.640）s，各進(jìn)行了一次循環(huán).

例26[32]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.795+1.030）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.608+0.858）s，各進(jìn)行了一次循環(huán).

例27[33]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（1.061+1.420）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.577+0.718）s，各進(jìn)行了一次循環(huán).

例28[21]329（Kober不等式）設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.702+0.390）s，各進(jìn)行了一次循環(huán).證明右端不等式（第一類(lèi)型不等式）耗時(shí)0.265 s，進(jìn)行了一次循環(huán).

例29[34]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.593+0.406）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.234+0.296）s，各進(jìn)行了一次循環(huán).

例30[34]設(shè)x∈（0，/2），則

證明左端不等式耗時(shí)（0.593+0.453）s，各進(jìn)行了一次循環(huán).證明右端不等式耗時(shí)（0.280+0.297）s，各進(jìn)行了一次循環(huán).

4　結(jié)語(yǔ)

借助于maple數(shù)學(xué)軟件和級(jí)數(shù)理論，本文研究了三角函數(shù)不等式的發(fā)現(xiàn)與機(jī)器自動(dòng)證明，提出了基于級(jí)數(shù)理論及多項(xiàng)式實(shí)根隔離的三角函數(shù)不等式自動(dòng)驗(yàn)證算法.該算法雖然不完備，但根據(jù)算法編寫(xiě)的試探性程序hdtrig2015能夠在極短時(shí)間內(nèi)實(shí)現(xiàn)三角函數(shù)不等式的自動(dòng)驗(yàn)證，且驗(yàn)證過(guò)程簡(jiǎn)單易懂，是“可讀”的，足見(jiàn)算法的優(yōu)越性.相較文獻(xiàn)[16]的區(qū)間分析的方法及文獻(xiàn)[17]的萬(wàn)能公式代換結(jié)合泰勒展開(kāi)的方法，本文的方法更為簡(jiǎn)單、直接、高效、具有更大的適用范圍，我們希望能進(jìn)一步發(fā)展此算法，以期解決更多傳統(tǒng)方法難以解決的問(wèn)題.

[1]楊路，侯曉榮，曾振柄.多項(xiàng)式的完全判別系統(tǒng)[J].中國(guó)科學(xué)：E輯，1996，26（5）：424-441.

[2]楊路.不等式機(jī)器證明的降維算法與通用程序[J].高技術(shù)通訊，1998，7：20-25.

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

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

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

[6]陳勝利，黃方劍.三元對(duì)稱(chēng)形式的Schur分拆與不等式的可讀證明[J].數(shù)學(xué)學(xué)報(bào)，2006，49（3）：491-502.

[7]楊路.差分代換與不等式機(jī)器證明[J].廣州大學(xué)學(xué)報(bào)（自然科學(xué)版），2006，5（2）：1-7.

[8]黃方劍.一類(lèi)多項(xiàng)式不等式的證明研究[J].科學(xué)技術(shù)與工程，2007，7（15）：3856-3859.

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

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

[11]陳勝利，姚勇，徐嘉.分拆降維方法和機(jī)器證明[J].系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（1）：26-34.

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

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

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

[15]楊路，郁文生，袁如意.一類(lèi)積分不等式的機(jī)器判定[J].中國(guó)科學(xué)：信息科學(xué)，2011，41（1）：48-65.

[16]邵俊偉，侯曉榮.InequalityProve及一個(gè)公開(kāi)問(wèn)題的求解[J].計(jì)算機(jī)工程與科學(xué)，2011，33（6）：114-117.

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

[18]李明，何燈.關(guān)于的較強(qiáng)上下界及其應(yīng)用[J].北京聯(lián)合大學(xué)學(xué)報(bào)（自然科學(xué)版），2010，24（2）：47-48.

[19]何燈，王少光，吳善和.關(guān)于Jordan不等式的拓廣及應(yīng)用[J].汕頭大學(xué)學(xué)報(bào)（自然科學(xué)版），2014，29（1）：24-32.

[20]Yang Z H.Unification and refinements of Jordan,Adamovi-Mitrinoviand and Cusa’s Inequalities[J/OL]. [2012-03-28].http：//arxiv.org/abs/1304.3180,2013.

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

[22]CHEN C P，CHEUNG W S.Sharpness of Wilker and Huygens type inequalities[J/OL].Journal of Inequalities and Applications.[2013-04-11].http：//www.journalofinequalitiesandapplications.com/content/2012/1/72.

[23]ZHANGL，ZHUL.AnewelementaryproofofWilker’sinequalities[J].MathematicalInequalities&Applications, 2007,11（1）：149-151.

[24]WU S H，SRIVASTAVA H M.A weighted and exponential generalization of Wilker’s inequality and its applications[J].Integral Transforms and Special Functions，2007，18（8）：529-535.

[25]王梓華.介紹一個(gè)Wilker型不等式[J].宜賓學(xué)院學(xué)報(bào)（自然科學(xué)版），2007，7（6）：21-22.

[26]祁鋒.Jordan和Kober不等式的拓廣與加強(qiáng)[J].工科教學(xué)，1996，12（4）：98-102.

[27]ZHUL.SharpeningJordan’s inequalityand the YangLe inequality[J].Applied Mathematics Letters，2006，19（3）：240-243.

[28]WU S H.Sharpness and generalization of Jordan’s inequality and its application[J].Taiwanese Journal of Mathematics，2008，12（2）：325-336.

[29]姜衛(wèi)東，華云.Jordan不等式的改進(jìn)及應(yīng)用[J].高等數(shù)學(xué)研究，2006，9（5）：60-61.

[30]ZHUL.SharpeningJordan’sinequalityandtheYangLeinequality,Ⅱ[J].AppliedMathematicsLetters,2006,19（9）：990-994.

[31]何燈，沈志軍.Jordan不等式的拓廣及應(yīng)用[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報(bào)（自然科學(xué)版），2011，29（5）：45-50.

[32]何燈，沈志軍.Jordan不等式的新型拓廣及應(yīng)用[J].廣東第二師范學(xué)院學(xué)報(bào)，2011，31（5）：23-30.

[33]何燈，沈志軍.Jordan不等式的拓廣及應(yīng)用Ⅱ[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報(bào)（自然科學(xué)版），2012，30（1）：19-23.

[34]祁峰，郭白妮.關(guān)于Kober不等式的推廣[J].焦作礦業(yè)學(xué)院學(xué)報(bào)，1993，12（4）：101-103.

The Finding and Automated Proving of the Univatiate Trigonometric Function Inequality

HE Deng,LI Yunjie
（Number 3 Middle School,Fuqing 350315,Fujian,China）

With the help of series theory and mathematical software-Maple，this paper studies the finding and automated proving of the univatiate trigonometric inequality.According to the algorithm program hdtrig 2015，the automatic proving is realized for the trigonometric function inequality.Many examples show that this algorithm has great superiority and can realize the machine automatic proving for a batch of trigonometric function inequality.

trigonometricfunction;inequality;Taylor expansion;machineproving;realrootisolation

O 211.67

A

1001-4217（2016）01-0024-11

2015-03-09

何燈（1984-），男，福建福清人，學(xué)士，中學(xué)教師，全國(guó)不等式研究會(huì)成員.研究方向：解析不等式及不等式機(jī)器證明.E-mail：hedeng123@163.com