帶約束條件多項(xiàng)式的差分代換及其應(yīng)用

劉保乾

（西藏自治區(qū)組織編制信息中心，西藏拉薩850000）

帶約束條件多項(xiàng)式的差分代換及其應(yīng)用

劉保乾

（西藏自治區(qū)組織編制信息中心，西藏拉薩850000）

對(duì)三角形幾何不等式判定算法agl進(jìn)行了改進(jìn)和補(bǔ)充，并根據(jù)這種算法設(shè)計(jì)了agl程序的升級(jí)版agl2009，討論了帶約束條件差分代換在證明根式型不等式中的應(yīng)用；給出了用agl程序發(fā)現(xiàn)的若干優(yōu)美的三角形幾何不等式.

差分代換；三角形幾何不等式；agl算法；機(jī)器證明

0 引言

筆者在文獻(xiàn)中介紹了2004年12月提出的用增量代換證明銳角三角形不等式的思想[1]，從而產(chǎn)生了帶約束條件多項(xiàng)式的差分代換問(wèn)題.此后又對(duì)這種思想做了進(jìn)一步闡述[2]和改進(jìn)[3-4]，得到了一種判定三角形幾何不等式的算法agl.編寫(xiě)的同名程序?qū)ε卸ㄈ切螏缀尾坏仁?，尤其是含有角平分線或半角三角函數(shù)的不等式十分有效，且在一些方面性能優(yōu)于Bottema軟件[5].本文擬對(duì)agl的算法進(jìn)行改進(jìn)和補(bǔ)充，并討論了帶約束條件差分代換在證明根式型不等式中的應(yīng)用.

以下約定：△ABC三邊為a、b、c，面積為Δ，角平分線、中線、高、傍切圓半徑分別為wa、wb、wc，ma、mb、mc，ha、hb、hc和ra、rb、rc，內(nèi)切圓和外接圓半徑分別為r和R，用∑表示循環(huán)和.另外，本文不等式驗(yàn)證環(huán)境均在Intel（R）Pentium（R）4 CPU 2.40 GHz，2.41 GHz，1.00 GB內(nèi)存環(huán)境下完成.

1 agl算法的改進(jìn)和補(bǔ)充

正如文獻(xiàn)［3］所述，agl不是一個(gè)完備的算法，對(duì)一些三角形幾何不等式可能失效.在解決這些失效不等式問(wèn)題的過(guò)程中，筆者發(fā)現(xiàn)如果對(duì)帶約束條件的多項(xiàng)式和條件同步進(jìn)行差分代換，可以部分地解決這個(gè)問(wèn)題.為了保證多項(xiàng)式和條件的同步性，通常將多項(xiàng)式f和條件u≥0寫(xiě)在一起構(gòu)成一個(gè)列表t=[f，u]，稱(chēng)這個(gè)列表為一個(gè)條件組.顯然條件組是由兩部分構(gòu)成，第一部分是多項(xiàng)式部分，用tf標(biāo)識(shí)；第二部分是約束條件部分，用tu標(biāo)識(shí).為證明不等式f≥0成立，需要用條件u對(duì)f按照agl算法進(jìn)行測(cè)試，稱(chēng)這個(gè)過(guò)程為對(duì)條件組t進(jìn)行正性測(cè)試.為了說(shuō)明agl算法的改進(jìn)思路，先介紹一下agl算法.

算法agl由文獻(xiàn)［3-4］可知，三角形幾何不等式的證明，最后可化為條件組w=的正性判定，由于agl算法要進(jìn)行多項(xiàng)式的相除運(yùn)算，故需要約定一個(gè)主變?cè)?，我們約定z是主變?cè)?算法agl的思路就是用w的tu部分去除tf部分差分代換集中的各個(gè)多項(xiàng)式，如果得到的商和余式均平凡非負(fù)，則可證得不等式f（m，n，z）≥0成立，如果商和余式中仍含有負(fù)系數(shù)項(xiàng)，則可繼續(xù)去除，直至得到的多項(xiàng)式中沒(méi)有負(fù)系數(shù)項(xiàng)，或者z的次數(shù)小于2為止.顯然算法agl總是可以終止的.但是要注意，當(dāng)temp2不為空時(shí)，輸出的多項(xiàng)式如果是半正定的，則f（m，n，z）≥0一定成立；輸出的多項(xiàng)式的正性若不可判定，則f（m，n，z）≥0可能成立也可能不成立，此時(shí)agl的算法失效.下面以條件組t=[f，u]為例，說(shuō)明agl算法的改進(jìn)思路.

1）對(duì)條件組t作差分代換.

2）條件組t的差分代換是一些新的條件組構(gòu)成的集合S.為了便于敘述和用程序控制，按代換結(jié)果的特征和約束條件，可將S中的條件組分成如下幾類(lèi).

i.如果條件組中tu部分的諸項(xiàng)系數(shù)全部為負(fù)數(shù)，則意味著出現(xiàn)了矛盾的結(jié)果（條件u≥0不能滿足），稱(chēng)此條件組為矛盾條件組.矛盾條件組應(yīng)當(dāng)放棄.出現(xiàn)這種情況的原因是，我們是按照差分代換全集的公式計(jì)算S的.以3元為例，多項(xiàng)式f（m，n，z）的差分代換（全集的）計(jì)算公式為[6]：在約束條件下，顯然z≤m，z≤n不會(huì)出現(xiàn)（否則會(huì)導(dǎo)出n≥m），這樣式（1）中的代換式f（m+z，m+n+z，z），f（m+n+z，m+z，z）就是多余的.

ii.如果條件組中tu部分的諸項(xiàng)系數(shù)全部為正數(shù)，而tf部分的諸項(xiàng)系數(shù)全部為負(fù)數(shù)，則意味著f≥0不成立，稱(chēng)這樣的條件組為反例條件組.顯然這里定義的反例條件組是一種極端反例，沒(méi)有包括tf部分含有正系數(shù)項(xiàng)的反例，是最遲出現(xiàn)的反例，這也是本改進(jìn)算法發(fā)現(xiàn)反例效率不高的主要原因之一.

iii.如果條件組中tf部分的諸項(xiàng)系數(shù)全部為正數(shù)，則稱(chēng)這樣的條件組為平凡條件組.

iv.如果條件組中tf和tu兩部分的系數(shù)均有正有負(fù)，則稱(chēng)這樣的條件組為待測(cè)組.集合中的絕大多數(shù)屬于待測(cè)組.

v.如果條件組中tu部分的系數(shù)全部為正，而tf部分的諸項(xiàng)系數(shù)有正有負(fù)，則意味著這個(gè)條件組中tf部分正半定的條件可以擴(kuò)大為任意正數(shù)，從而把條件不等式化為關(guān)于正數(shù)的不等式，稱(chēng)這樣的條件組為正數(shù)組.很顯然，正數(shù)組的條件可以去掉成為普通的多項(xiàng)式不等式，但是否成立仍需要進(jìn)一步判定.

vi.在算法agl中，由于考慮的是單個(gè)條件組的正性判定，tu部分的條件保持不變，故不需要對(duì)條件多項(xiàng)式進(jìn)行檢測(cè).但對(duì)條件組做逐次差分代換[7]過(guò)程中，tu部分要發(fā)生變化.如果tu部分主變?cè)罡叽蔚南禂?shù)出現(xiàn)字母，則多項(xiàng)式相除運(yùn)算會(huì)產(chǎn)生分式，此時(shí)可能會(huì)產(chǎn)生一些不可預(yù)料的結(jié)果，這種條件組對(duì)agl算法來(lái)講是有瑕疵的.稱(chēng)tu部分主變?cè)罡叽蔚南禂?shù)出現(xiàn)字母的條件組為瑕疵組.如果出現(xiàn)瑕疵組，則輸出相關(guān)信息并轉(zhuǎn)入人工處理.

3）對(duì)S中符合2）的諸類(lèi)型條件組進(jìn)行過(guò)濾，以排除極端情形，尋找反例，并轉(zhuǎn)入不同的處理流程.

4）按照agl算法，用待測(cè)組中的tu部分對(duì)tf部分進(jìn)行正性測(cè)試，如果測(cè)試成功，則將該待測(cè)組拋棄.

5）對(duì)正數(shù)組的正性進(jìn)行機(jī)器或人工測(cè)試.

6）如果某個(gè)待測(cè)組的正性不易判定，則可嘗試給這個(gè)待測(cè)組作逐次差分代換，對(duì)代換結(jié)果再進(jìn)行測(cè)試，以確定正性或進(jìn)一步尋找反例條件組.

根據(jù)上述思路，下面以3元多項(xiàng)式為例，給出agl的改進(jìn)算法ag.以下用?（f）表示多項(xiàng)式f的次數(shù).

算法ag算法ag過(guò)程如下.

A1）設(shè)有3元齊次多項(xiàng)式不等式f（x，y，z）≥0，滿足約束條件g（x，y，z）≥0，且?（g）≤?（f）.

A2）建立初始條件組[f（x，y，z），g（x，y，z）]，并置入集合變量o中，得條件組集o={[f（x，y，z），g（x，y，z）]}；為保存o變量的狀態(tài)，同時(shí)將o置入temp1中.

A3）對(duì)temp1作差分代換，并將代換結(jié)果置入temp1之中.

A4）對(duì)temp1中的矛盾條件組、平凡條件組進(jìn)行過(guò)濾，剩余部分仍置于temp1中.

A5）檢測(cè)temp1中的反例條件組，如果有，輸出反例并停機(jī).

A6）檢測(cè)temp1中的瑕疵條件組.

A6.1）如果有瑕疵條件組，則連續(xù)做若干次（本文程序中設(shè)置為5次）逐次差分代換，并對(duì)每次代換尋找反例.若有反例，則輸出反例并停機(jī)；無(wú)反例，則輸出人工處理提示信息，停機(jī).

A6.2）如果沒(méi)有瑕疵條件組，則對(duì)temp1中的條件組按agl算法進(jìn)行正性測(cè)試，將測(cè)試成功的條件組拋棄，剩余的部分仍置于temp1之中.

A7）檢測(cè)temp1是否為空集，如果是，則輸出不等式成立的信息并停機(jī)；如果不是，則轉(zhuǎn)向A3.

可以看出，ag算法的終止性是不能保證的，這是因?yàn)椋阂皇莂g算法的終止是有缺陷的，這一點(diǎn)可以由A6.1看出，因?yàn)閷?duì)于f（x，y，z）≥0成立但ag無(wú)法判定的情形，不可能輸出反例，這樣程序會(huì)進(jìn)入死循環(huán)，為了避免這種情況，程序中設(shè)置了測(cè)試次數(shù);二是當(dāng)f（x，y，z）≥0成立但逐次差分代換過(guò)程中又沒(méi)有出現(xiàn)瑕疵條件組時(shí)（相當(dāng)于A6.2時(shí)段），程序無(wú)法自動(dòng)終止，此時(shí)要強(qiáng)制停機(jī)，轉(zhuǎn)入人工處理，這也是ag算法的最大缺點(diǎn).后面的例11演示了人工處理的例子.

2 三角形幾何不等式判定程序agl2009

根據(jù)ag算法，筆者編寫(xiě)了三角形不等式判定程序agl2009（源程序見(jiàn)http://www.irgoc.org/viewtopic.php?f=27&t=121&sid=ddaa5759422763f544551e5962898c69或http://www.mathlinks.ro/Forum/viewtopic.php?p=1705932#1705932）.它可以看作是文獻(xiàn)［3－4］中agl程序的升級(jí)版本，因?yàn)樗粌H兼顧了agl的功能，而且還增加了許多新功能.

2.1 agl2009程序的功能及命令格式

agl2009是在Maple平臺(tái)上開(kāi)發(fā)的應(yīng)用程序，專(zhuān)門(mén)對(duì)三角形幾何不等式進(jìn)行判定.首先將agl2009拷貝到Maple的安裝目錄下，在進(jìn)入Maple環(huán)境后就可以運(yùn)行這個(gè)程序.具體運(yùn)行指令是read`agl2009.txt`，執(zhí)行了這個(gè)指令，就可以使用agl2009了.

auto命令

功能：對(duì)一個(gè)三角形幾何不等式f（△ABC）≥0，作角代換A→π-2A，B→π－2B，C→π-2C，并將代換式化為用三角形邊長(zhǎng)表示的形式，輸出這個(gè)代換式的分子w1和分母w2，而且w1和w2已經(jīng)取掉了平凡非負(fù)因式.

指令格式：auto（ineq），其中ineq表示一個(gè)待判定正性的三角形幾何量表達(dá)式.

例1判定wa-ha的正性.判定步驟如下：

＞read`agl2009.txt`；#讀入agl2009程序.

＞wa-ha；#鍵入欲判定不等式表達(dá)式.

＞auto（%）；#%表示前次輸入的式子wa-ha，即對(duì)wa-ha施行auto命令.

執(zhí)行上述命令后，顯示出用雙線隔開(kāi)的兩組多項(xiàng)式，前組多項(xiàng)式表示對(duì)wa-ha施行角代換后，得到式子的分子和分母；后組表示取掉平凡非負(fù)因式后的分子和分母.之所以顯示前一組，是為了觀察到更多的信息（如不等式的取等號(hào)條件等）.

特別值得一提的是，如果w1=0，則預(yù)示著發(fā)現(xiàn)了一個(gè)三角形恒等式.此時(shí)程序自動(dòng)出現(xiàn)“The Inequality may be an identity!”提示.

需要指出的是，auto命令對(duì)一些三角形幾何量表達(dá)式（如含有中線奇次方，根式型幾何量和有理式混合等情形）不能自動(dòng)完成有理化，此時(shí)要想辦法進(jìn)行人工有理化.

agl命令

功能：對(duì)一個(gè)用三角形邊長(zhǎng)表示的多項(xiàng)式正性進(jìn)行判定.對(duì)不成立者能夠自動(dòng)輸出反例條件組；對(duì)不能判定者，可以輸出一些提示信息.

指令格式：agl（ineq），或者agl（ineq，[ineqs]），其中ineq表示一個(gè)用三角形邊長(zhǎng)表示的多項(xiàng)式；ineqs表示一個(gè)條件，目前只能接受aa參數(shù)，表示三角形為銳角三角形.

需要指出的是，在agl模塊中設(shè)置了全局變量o.當(dāng)程序判定不成功時(shí)，變量o能夠帶出初始條件組的差分代換集，以便于人工進(jìn)行分析.

qht命令

功能：尋找一些特殊退化條件下取等號(hào)的不等式的最佳系數(shù)，這個(gè)方法是試探性的.這個(gè)模塊應(yīng)用了文獻(xiàn)[8]提供的恒等式.它本質(zhì)上是利用了退化三角形＜1，1，2＞，＜1，1，0＞，或者銳角三角形退化為等腰直角三角形.

指令格式：subs（qht，ineq），其中ineq表示一個(gè)對(duì)應(yīng)于三角形幾何不等式的表達(dá)式.

例2確定三角形幾何量表達(dá)式f1-kf2中可能有的最佳系數(shù)，需輸入下面的指令:

＞w:=subs（qht，f1-k*f2）；#將所給表達(dá)式代換后賦給變量w，以便于調(diào)用.

＞solve（subs（x=0，w），k）；#嘗試退化條件＜1，1，0＞時(shí)可能有的最佳值.

＞solve（subs（x=1，w），k）；#嘗試退化條件＜1，1，2＞時(shí)可能有的最佳值.

>so lv e（su b s（x=sq rt（2）/2，w），k）；#嘗試銳角三角形退化為等腰直角三角形時(shí)的情形.

所有這些最佳值得到后，均要用a g l2 0 0 9或其他軟件進(jìn)行驗(yàn)證確認(rèn).

e q命令

功能：尋找三角形幾何不等式一些特殊的取等號(hào)條件.

指令格式：e q（in e q）.注意在用e q找取等號(hào)條件時(shí)，應(yīng)通過(guò)平方運(yùn)算盡量將根式化掉.

te stf命令

功能：用三角形邊長(zhǎng)的經(jīng)驗(yàn)數(shù)據(jù)驗(yàn)證不等式.

指令格式：te stf（in e q，[a，b，c]），其中in e q表示不等式對(duì)應(yīng)的表達(dá)式，a，b，c表示三角形邊長(zhǎng)的驗(yàn)證數(shù)據(jù).

te stf命令雖然不能判定不等式是否成立，但它作為一個(gè)驗(yàn)證命令還是十分有用的.

a g g命令

功能：對(duì)單個(gè)的條件組按照a g l算法進(jìn)行測(cè)試.如果條件組的正性得到判定，返回-1，否則返回1.

指令格式：a g g（lst），其中l(wèi)st表示一個(gè)條件組.

sd sd命令

功能：對(duì)條件組構(gòu)成的集合進(jìn)行差分代換，并進(jìn)行正性測(cè)試.

指令格式：sd sd（in e q），其中in e q表示一個(gè)條件組集.

a b c to x命令

功能：將一個(gè)三角形幾何量表達(dá)式化為關(guān)于正數(shù)x，y，z的形式.

指令格式：sd sd（in e q），其中in e q表示一個(gè)三角形幾何量表達(dá)式.

命令a g g、sd sd和a b c to x均是為了方便人工處理而設(shè)計(jì)的.

2.2 a g l2 0 0 9程序應(yīng)用舉例

例3（文獻(xiàn)[9]中的l5 8）在△A B C中，證明

證明用a g l2 0 0 9程序證明如下：

>g:=w b*w c/（2*ra+w a）-2*（b+c）*a*r/（（a+b）*（a+c））；#輸入不等式表達(dá)式.

>a u to（%）；#由顯示的w 1知，不等式（2）有取等號(hào)條件b=c.

由于程序?qū) 1和w 2取平凡非負(fù)因式后，均已經(jīng)是正數(shù)，故不等式（2）成立.

由w1的表達(dá)式知，不等式（2）有取等號(hào)條件b=c，現(xiàn)用e q命令再找一些不等式（2）的取等號(hào)條件.輸入命令e q（g），則顯示：

根據(jù)此提示信息可找到不等式（2）的部分取等號(hào)條件為{a+c=b}，{b=c}，{a+b=c}.

例4在△A B C中，確定不等式ma≥ha的取等號(hào)條件.

解運(yùn)行e q（m a-h a）命令后，得到部分取等號(hào)條件為：

可以看出，第1個(gè)取等號(hào)條件特別有趣.

例5在銳角△ABC中，證明

解輸入以下命令序列：

>（sgm(wa*b））^2-（sqrt（3）/2*sgm（a*b））^2；#為便于有理化，對(duì)不等式兩邊要同時(shí)平方.>auto（%）；

>agl（w1，[aa]）；#由于是銳角三角形，故要帶aa參數(shù).

經(jīng)過(guò)數(shù)秒運(yùn)算后，打印出“The inequality holds”，故不等式（3）成立.

解鍵入以下命令序列：

>sgm（（hb-hc）^2）-k*sgm（（wb-wc）^2）；

>subs（qht，%）；#qht的本質(zhì)是根據(jù)文獻(xiàn)［8］建立的公式集.

>factor（subs（x=sqrt（2）/2，solve（%，k）））；則顯示：

用agl具體驗(yàn)證知，當(dāng)k=0.6時(shí)成立，但k=0.61時(shí)不成立（用Bottema軟件否定）.雖然這里未能?chē)?yán)格證明這個(gè)常數(shù)就是最佳值，但這個(gè)結(jié)果仍然讓人鼓舞，因?yàn)橛闷渌浖请y以得到這種結(jié)果的.

例7證明恒等式

證明運(yùn)行auto命令后發(fā)現(xiàn)w1=0，故式（4）是一個(gè)恒等式.

例8設(shè)k∈R，證明含參不等式

證明不等式（5）化為關(guān)于k的一元二次不等式

用agl易證二次項(xiàng)系數(shù)非負(fù)，判別式為-4g，其中g(shù)=（-bwa+awa-cwb+bwb+cwc-awc）·（-cwa+awa-awb+bwb+cwc-bwc），用agl易證g≥0成立，由此證得不等式（5）.

例9試對(duì)不等式

進(jìn)行判定.

解運(yùn)行agl（w1）命令后，數(shù)秒給出反例多項(xiàng)式.而運(yùn)行帶銳角參數(shù)的命令agl（w1，[aa]），很快判定式（6）在銳角三角形中成立.

注如果用Bottema軟件尋找不等式（6）的反例，程序運(yùn)行2 697 s后仍然沒(méi)有結(jié)束跡象.由此可見(jiàn)，agl2009在發(fā)現(xiàn)和探討三角形不等式方面，有一些不可替代的作用.例10在△ABC中，證明不等式

證明不等式（7）兩邊同時(shí)平方，并運(yùn)行agl（w1）命令后，發(fā)現(xiàn)w1中有因式（a-b）2·（b-c）2（c-a）2，故知不等式（7）在等腰三角形時(shí)取等號(hào)（這類(lèi)不等式一般非常強(qiáng)），其余證明略.

例11在△ABC中，證明不等式

證明鍵入agl（w1）命令后，判定沒(méi)有成功，轉(zhuǎn)入人工處理.經(jīng)檢查知，全局變量o中有一個(gè)條件組，且是一個(gè)正數(shù)組，故證明不等式（8）轉(zhuǎn)化為證明o中正數(shù)組的tf部分關(guān)于正數(shù)m，n，z成立，而這可以用文獻(xiàn)中的第二類(lèi)差分代換程序完成[10].

3 帶約束條件差分代換的其他應(yīng)用

應(yīng)用帶約束條件多項(xiàng)式的差分代換方法，可以將一些根式形式且不易有理化的三角形幾何不等式問(wèn)題轉(zhuǎn)化為條件不等式加以解決.

例12在△ABC中，證明

證明不等式（9）等價(jià)于如下條件不等式：

對(duì)此條件不等式進(jìn)行代數(shù)化，得到一個(gè)條件組[f1，f2]（表達(dá)式略）.對(duì)條件組[f1，f2]進(jìn)行一次差分代換，得到由3個(gè)條件組構(gòu)成的差分代換集.用agg命令對(duì)這3個(gè)條件組一一進(jìn)行檢測(cè)，結(jié)果發(fā)現(xiàn)其中有2個(gè)是半正定的，另外1個(gè)正性不能判定.對(duì)這個(gè)正性不能判定的條件組繼續(xù)作差分代換，用agg對(duì)得到的條件組進(jìn)行測(cè)試，結(jié)果發(fā)現(xiàn)全部是正半定的，故不等式（9）成立.

例13在△ABC中,證明

證明不等式（10）可化為條件不等式

這個(gè)條件不等式代數(shù)化后可化為一個(gè)條件組，對(duì)這個(gè)條件組作一次差分代換，得到條件組集合（為節(jié)約篇幅，這里僅寫(xiě)出了部分表達(dá)式）：

其中，

顯然w中有2個(gè)正數(shù)組，其中g(shù)3≥0容易用逐次差分代換程序sds[7]判定成立，g1≥0不容易直接判定，但經(jīng)過(guò)倒數(shù)代換加速[10]后容易判定.經(jīng)驗(yàn)證知，剩余的條件組[g2，gu]的正性不能用agl算法判定，故這里我們未完成對(duì)不等式（10）的證明.

由例13可以看出，一般條件不等式的證明是十分復(fù)雜的.如何對(duì)由式（11）決定的條件組[g2，gu]的正性進(jìn)行判定仍是一個(gè)待解決的問(wèn)題.

4 用agl2009程序發(fā)現(xiàn)的優(yōu)美不等式

截至目前，用agl2009程序已經(jīng)發(fā)現(xiàn)了500多個(gè)優(yōu)美的三角形幾何不等式，這些不等式加強(qiáng)或隔離了一些著名的結(jié)果，而且其中的許多結(jié)果是用其他軟件難以判定的.下面摘錄若干個(gè)形式比較優(yōu)美的結(jié)果（更多結(jié)果見(jiàn)http://www.mathlinks.ro/Forum/viewtopic.php?t=315511），同時(shí)注明用agl2009程序驗(yàn)證所花費(fèi)的時(shí)間（這些不等式如果用Bottema軟件驗(yàn)證，大多數(shù)時(shí)間超長(zhǎng)或不能驗(yàn)證）.

5 結(jié)語(yǔ)

本文給出的算法ag，較好地改進(jìn)了agl算法的不足，據(jù)此編寫(xiě)的程序agl2009適用于一大類(lèi)三角形幾何不等式的判定.從使用情況看，由于agl2009程序運(yùn)行速度提高，形成了人的思維和判定結(jié)果同步和互動(dòng)的局面，這使得一些難度甚大且形式新穎的優(yōu)美不等式被發(fā)現(xiàn)（事實(shí)證明，如果不等式證明器的運(yùn)行時(shí)間過(guò)長(zhǎng)，將會(huì)使預(yù)熱了的思維冷卻和遲滯，瞬間產(chǎn)生的靈感火花由于等待而減弱或熄滅，從而使研究效率和質(zhì)量大打折扣）.雖然如此，agl2009程序尚存在以下不足或問(wèn)題：一是agl2009給出的反例是條件組，是一種間接反例；二是對(duì)于有些不等式，agl2009輸出反例的時(shí)間過(guò)長(zhǎng)，而從算法分析來(lái)看，反例條件組作為最遲出現(xiàn)的反例，是有改進(jìn)余地的；三是agl2009的終止性是有缺陷的.另外，由本文可以看出，對(duì)于agl算法失效的情形，逐次差分代換不是總能奏效的.如何建立一般條件不等式的判定算法和程序，并向多元進(jìn)行推廣，這些都是十分有價(jià)值的研究課題.

最后再提幾個(gè)有趣的不等式問(wèn)題：

[1] 劉保乾.三角形幾何不等式新探[J].不等式研究通訊，2009，16（4）：440-451.

[2] 劉保乾.不等式研究的幾個(gè)新結(jié)論和新問(wèn)題[J].嘉應(yīng)學(xué)院學(xué)報(bào)，2008，26（6）：19-26.

[3]劉保乾.銳角三角形幾何不等式的差分代換證法及應(yīng)用程序[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報(bào)，2009，27（5）：33-38.

[4] 劉保乾.條件Si類(lèi)多項(xiàng)式的構(gòu)造及其他[J].廣東教育學(xué)院學(xué)報(bào)，2009，29（5）：8-13.

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

[6] 劉保乾.用差分代換研究實(shí)數(shù)域中多項(xiàng)式的半正定性[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報(bào)，2008，26（2）：8-11.

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

[8] 闕浩濤.否定三角形不等式猜想的一種方法[M]//劉保乾.Bottema，我們看見(jiàn)了什么——三角形幾何不等式研究的新理論、新方法和新結(jié)果.拉薩：西藏人民出版社，2003：552-556.

[9] 劉保乾.100個(gè)優(yōu)美的三角形不等式新問(wèn)題[M]//中國(guó)初等數(shù)學(xué)研究（第1輯）.哈爾濱：哈爾濱工業(yè)大學(xué)出版社，2009：92-95.

[10] 劉保乾.再談第二類(lèi)差分代換[J].佛山科學(xué)技術(shù)學(xué)院學(xué)報(bào)，2009，27（2）：1-6.

Constrained Polynomial Differential Substitution and Applications

LIU Bao-qian
(Information Center，Department of Personnel，Tibet Autonomous Region，Lasa 850000，Tibet，China)

Geometric inequality algorithm is improved and an upgraded version agl2009 isdesigned.Constrainedpolynomial differential substitution isstudied for square root inequalityand several geometric inequalities are found by the agl algorithm.

differential substitution；geometric inequality algorithm；agl algorithm；machine proofing

O 122.3

A

1001-4217（2010）02-0001-10

2009-11-24

劉保乾（1962-），男，陜西鳳翔人，計(jì)算機(jī)本科.研究方向：多項(xiàng)式不等式與機(jī)器證明.E-mail：wshr987@163.com