徐 嘉(西南民族大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，四川 成都 610041)

三類根式不等式的有理化與機(jī)器證明

徐 嘉
(西南民族大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，四川 成都 610041)

摘 要：研究了三類根式不等式的有理化與機(jī)器證明.首先給出了三類根式不等式成立的充分必要條件，即等價(jià)的有理不等式組.然后介紹了伴隨多項(xiàng)式概念，并建立了一個(gè)算法SimplexM.SimplexM能夠處理帶有連結(jié)詞∧(and)和∨(or)的多項(xiàng)式不等式組.最后給出了大量的應(yīng)用實(shí)例，證實(shí)了這一方法的有效性.

關(guān)鍵詞：根式不等式；有理化；單純剖分方法

根式不等式的自動(dòng)證明是定理機(jī)器證明中的熱點(diǎn)和難點(diǎn).通用的方法是使用一些消去手段(如Groebner基，結(jié)式等)去除根式，然后轉(zhuǎn)化為相應(yīng)的實(shí)量詞公式加以解決.其中值得特別注意的是楊路的降維方法[1，2，3].它的特點(diǎn)是不增加新的變?cè)?，保持較低的維數(shù)，從而有非常高的運(yùn)行效率.根據(jù)其方法編制的軟件Bottema是目前最為常用的不等式證明軟件，已為國內(nèi)外廣大不等式研究者所熟悉.但是對(duì)于一些比較特殊的根式不等式類，仍然需要更加精細(xì)的研究，以進(jìn)一步提高證明的效率.在文[4]中由本文作者及合作者給出了一類根式不等式的高效算法.它的主要思想是基于”有理化＋差分代換”的證明模式.其中有理化步驟是依賴于如下的結(jié)果.

定理(楊路)設(shè)u，v，w，t都是非負(fù)實(shí)數(shù)，則不等式

成立的充分必要條件是下列c0，c1，c2，c3都成立

其中σ1= u＋v＋w，σ2= uv＋vw＋wu，σ3= uvw.

上述定理中的c0包含了一類代數(shù)數(shù)的極小多項(xiàng)式，相關(guān)的三角代數(shù)數(shù)的極小多項(xiàng)式計(jì)算方法可參考文獻(xiàn)[5].

使用上述楊路定理加差分代換方法可以很容易證明如下這類較為困難幾何不等式

其中ha是三角形a邊上對(duì)應(yīng)的高線長度，wb是b邊上對(duì)應(yīng)的角平分線長度，mc是c邊上對(duì)應(yīng)的中線長度，R，r分別是三角形的外接圓半徑和內(nèi)切圓半徑.設(shè)x，y，z是正實(shí)數(shù)，令

則有

于是需要證明的幾何不等式就轉(zhuǎn)化為了含變?cè)獂，y，z形如

的代數(shù)不等式.然后使用楊路定理進(jìn)一步轉(zhuǎn)化為證明4個(gè)代數(shù)不等式同時(shí)成立，對(duì)最終的代數(shù)不等式使用逐次差分代換方法證明.

但是這一方法在處理形如

類型的根式不等式會(huì)遇到困難.由楊路定理可見，不等式

是等價(jià)于公式

本文中∧，∨分別代表邏輯連接詞”且(and)”，”或(or)”.注意到當(dāng)c0，c1，c2，c3是實(shí)函數(shù)時(shí)(不妨假設(shè)變?cè)莤，變化范圍是Ω)，上面的公式就會(huì)帶有一個(gè)實(shí)量詞?(任意)，可是量詞公式

并不等價(jià)于

明顯有φ2?φ1.

差分代換方法雖然適用于φ2，但是φ1成立時(shí)公式φ2也成立的概率很小.這導(dǎo)致”有理化＋差分代換方法”模式在證明這類根式不等式時(shí)成功的概率極低，幾乎失效.在本文中，我們將要解決這個(gè)困難.主要的思路是將變?cè)目臻g進(jìn)行單純分解，當(dāng)空間被足夠的細(xì)分之后，在每一個(gè)小的單純形上，可以期望公式φ2是成立的.此外，我們還將給出另一類根式不等式的的有理化，即

同時(shí)對(duì)

類型的不等式給出不同于前述楊路定理的有理化等價(jià)條件.

1 三類根式不等式的有理化

首先，我們需要如下的引理

引理1 u，v，w，t都是非負(fù)實(shí)數(shù)，如下的等價(jià)關(guān)系成立

其中

證明?注意到不等式

如果成立，則u，v，w，t只能有三種大小關(guān)系，即

兩邊平方得

兩邊平方得

?將上面證明過程倒推即可.

應(yīng)用基本引理，我們可以證明下面的結(jié)果.

定理1 u，v，w，t都是非負(fù)實(shí)數(shù)，如下的等價(jià)關(guān)系成立

其中

證明將

兩端平方，直接應(yīng)用引理1即可.

定理2 u，v，w，t都是非負(fù)實(shí)數(shù)，如下的等價(jià)關(guān)系成立

其中

證明?對(duì)

兩端平方，立得0≤R1.

將(1. 4)變形為

明顯上式兩端都是正實(shí)數(shù)，兩端平方不等號(hào)仍保持，即有

上式變形為

由于0≤R1，推知有(w＋t) - (u＋v)≥0 .因此(1.5)兩端仍是正實(shí)數(shù)，再次兩端平方，得到

由此推得0≤R2.

(1.6)可變形為

兩端平方，立得R3≥0 .

?將上面證明過程倒推即可.

討論:定理2的結(jié)論與文獻(xiàn)[4]中楊路的結(jié)果不同.這里的結(jié)論更簡單，并且少一個(gè)多項(xiàng)式.

從定理2，立即推出下面的結(jié)論.

定理3 u，v，w，t都是非負(fù)實(shí)數(shù)，如下的等價(jià)關(guān)系成立

其中

定理1，2，3實(shí)現(xiàn)在三類根式不等式的有理化.下一節(jié)將討論如何檢測有理化后的條件是否成立.

2　單純剖分方法

幾何量(如體積，邊長等等)通常是與坐標(biāo)選擇無關(guān)的，故涉及幾何的不等式在某些空間變換(如旋轉(zhuǎn)變換)下保持不變，所以當(dāng)這些不等式被轉(zhuǎn)化為等價(jià)的代數(shù)不等式后成為齊次型不等式.研究具有齊次性的函數(shù)，往往只需考慮變?cè)跇?biāo)準(zhǔn)單形上的變化情況就足夠了.單純剖分方法就是基于標(biāo)準(zhǔn)單形的單純剖分的.它是從逐次差分代換方法[6，7，8]啟發(fā)而來的.

點(diǎn)的坐標(biāo)采用列向量.標(biāo)準(zhǔn)單形記為Δn，

標(biāo)準(zhǔn)單形的一個(gè)單純剖分是指單純形

滿足

并且Λ1，…，Λm內(nèi)部不相交.

單純剖分可以迭代，形成逐級(jí)的單純剖分.關(guān)鍵之處在于，逐級(jí)的單純剖分有代數(shù)產(chǎn)生方式.注意到單純形Λ?Δn對(duì)應(yīng)著一個(gè)矩陣，矩陣的列是單純形的頂點(diǎn)坐標(biāo)(列向量)，記為[Λ] .這個(gè)對(duì)應(yīng)不是唯一的，因?yàn)轫旤c(diǎn)可以任意排序.也就是說如果兩個(gè)矩陣只相差一個(gè)列置換，則它們是同一個(gè)單純形的對(duì)應(yīng)矩陣.反過來列隨機(jī)矩陣M，如果其行列式｜M｜≠0，則M的列可張成單純形，記為Con(M)，M的列是單純形的頂點(diǎn).

引理2 如果單純形Λ1，…，Λm?Δn是標(biāo)準(zhǔn)單形的一個(gè)單純剖分，則

引理2也就是說，當(dāng)σ1，…，σk都取遍集合{1，2…，m}中的所有數(shù)，則單純形

的集合也是標(biāo)準(zhǔn)單形Δn的單純剖分.

特別地，考慮單純形的重心剖分[8].記n×n三角矩陣

矩陣G被稱為重心矩陣，如果G可由矩陣Gn通過行置換得到.重心矩陣共有n!個(gè).即

其中Sn是集合{1，2…，n}上的全對(duì)稱置換群，Pσ是置換σ對(duì)應(yīng)的置換矩陣.

容易看到任意單形Λ有如下分解式(Λ的重心剖分)

特別地對(duì)標(biāo)準(zhǔn)單形有

三階的6個(gè)重心矩陣如下

它們對(duì)應(yīng)的單純形如圖1.

圖1　標(biāo)準(zhǔn)單形Δ3的重心剖分Fig.The barycentric subdivision of Δ3

為了使用單純剖分去證明不等式，一個(gè)關(guān)鍵的概念是多項(xiàng)式在單純形上的伴隨多項(xiàng)式.它的定義如下

定義1 給定多項(xiàng)式f∈R[x1，…，xn]和單純形Λ?Δn，多項(xiàng)式f([Λ] (x1，…，xn)T)被稱為多項(xiàng)式f在單純形Λ上的伴隨多項(xiàng)式.

伴隨多項(xiàng)式有如下的基本性質(zhì).

引理3 給定多項(xiàng)式f∈R[x1，…，xn]和單純形Λ?Δn，則

f([Λ]x)可能會(huì)有非常簡單的特征，例如所有系數(shù)都是非負(fù)實(shí)數(shù).這個(gè)特征正是逐次差分代換方法的出發(fā)點(diǎn)[6，7，8].伴隨多項(xiàng)式相關(guān)的其它應(yīng)用還可見[9].

3　算法

讓我們從一個(gè)比較簡單的例子出發(fā)，來介紹單純剖分方法的具體操作步驟.

例1 證明如下根式不等式

其中

證明第一步，令

原不等式轉(zhuǎn)化為證明

利用定理3，我們需要證明

其中

第二步，取標(biāo)準(zhǔn)單形的一階重心剖分(圖1)，下面對(duì)每一個(gè)小單形驗(yàn)證公式(3.1)是否成立.

計(jì)算多項(xiàng)式R1，R2，R3相對(duì)于單純形Λ1的伴隨多項(xiàng)式

其中X = (x，y，z)T.我們會(huì)發(fā)現(xiàn)R3([Λ1]X)的系數(shù)全是負(fù)實(shí)數(shù)，也就是說在單純形Λ1上R3≤0成立，因此量詞公式

是成立的.完全類似地，可以驗(yàn)證公式

都是成立的，所以公式(3.1)成立.原不等式得證.

討論:例1僅僅只對(duì)標(biāo)準(zhǔn)單形做了一次剖分就成功了.如果對(duì)Λi，i = 1，…，6，伴隨多項(xiàng)式

都沒有出現(xiàn)所有系數(shù)全是負(fù)實(shí)數(shù)，則需要再對(duì)Λi繼續(xù)剖分成更小的單純形，再做驗(yàn)證.直到對(duì)每一個(gè)小單形Λ，R1([Λ]X)，R2([Λ]X)，R3([Λ]X)至少有一個(gè)出現(xiàn)所有系數(shù)全是負(fù)實(shí)數(shù)(判斷出原不等式成立)，或者出現(xiàn)存在一個(gè)小單形Λ使得三個(gè)多項(xiàng)式R1([Λ]X)，R2([Λ]X)，R3([Λ]X)的系數(shù)全是正實(shí)數(shù)(原不等式不成立)為止.

下面我們來建立算法SimplexM.考慮兩種基本的量詞公式(其它的量詞公可以由它們復(fù)合而成)

其中fi∈R[x1，…，xn]都是齊次的.我們可以仿照定義1，定義基本公式的伴隨公式如下

定義2 給定原子公式ψ和單純形Λ?Δn，公式ψ([Λ] (x1，…，xn)T)被稱為ψ在單純形Λ上的伴隨公式.

定義3

①稱公式f≥0(≤0)在單純形Λ?Δn上是顯式成立的，如果伴隨多項(xiàng)式f([Λ]X)的系數(shù)全部都是正(負(fù))的實(shí)數(shù).

②稱公式f≥0(≤0)在單純形Λ?Δn上是顯式矛盾的，如果伴隨多項(xiàng)式f([Λ]X)的系數(shù)全部都是負(fù)(正)的實(shí)數(shù).

③稱原子公式ψ1在單純形Λ上是顯式成立(矛盾)的，如果ψ中的每一個(gè)(存在一個(gè))子公式是顯示成立(矛盾)的.

④稱原子公式ψ2在單純形Λ上是顯式成立(矛盾)的，如果ψ中存在一個(gè)(每一個(gè))子公式是顯示成立(矛盾)的.

定義4 給定n×n的矩陣M，定義集合

算法SimplexM

輸入:量詞公式ψ(ψ1或ψ2).

Step1.設(shè)置初始集合S = {Gσ｜σ∈Sn} .

Step2.對(duì)S中的每一個(gè)元素計(jì)算公式ψ的伴隨公式ψ(GσX)，并且記所有的使公式ψ(GσX)是非顯式成立的矩陣組成集合Temp.

Step2.1.如果Temp是空集，則輸出”公式ψ成立”

Step2.2.如果Temp中含有公式是顯式矛盾的，則輸出:”公式ψ不成立”.

Step2.3.否則令

重復(fù)Step2.

程序結(jié)束.

4　實(shí)驗(yàn)

使用著名數(shù)學(xué)軟件Maple平臺(tái)，我們實(shí)現(xiàn)了上述的算法SimplexM.對(duì)大量的形如

的根式不等式作了計(jì)算.由于

類型的例子在文獻(xiàn)[4]已作了大量列舉.下面主要列舉了另外兩種類型的例子.其中的幾何不等式需要轉(zhuǎn)化為等價(jià)的代數(shù)不等式，轉(zhuǎn)化需要的公式表可見文獻(xiàn)[4].這些例子主要來自文獻(xiàn)[10 - 12].所有例子都是在一臺(tái)筆記本電腦上運(yùn)行測試，基本的硬件配置是:2.5GHz-Intel(R)Core(TM)i5-3210M，內(nèi)存4G，操作系統(tǒng)為windows 7.

表1　實(shí)驗(yàn)的例子與測試時(shí)間Table 1 experiments and test time

5　結(jié)語

本文中，我們提出了一個(gè)方法去證明三類根式不等式.方法主要分兩步①是有理化，②是使用單純剖分方法驗(yàn)證相應(yīng)的實(shí)量詞公式.它進(jìn)一步擴(kuò)展了”有理化＋差分代換”的模式而成為”有理化＋單純剖分”的模式.利用這一方法，我們成功的證明了超過200個(gè)例子，其中一些是公開問題.這種思想(剖分方法)還被應(yīng)用于解決其它的問題，如判定copositive矩陣[13]等等.

參考文獻(xiàn)

[1]YANG LU，XIA SHI HONG.Automated Proving for a Class of Constructive Geometric Inequalities [J].Chinese Journal of Computers，2003，26(7):769-778.

[2]YANG LU，XIA BI CAN.Automated Proving and Discovering on Inequalities(in Chinese)[M].Beijing:Science Press，2008.

[3]YANG LU，XIA SHI HONG.An Inequality-proving Program Applied to Global Optimization [C].In:Yang W C et al eds.Proceedings of the A-sian Technology Conference in Mathematics.Blacksbug: ATCM，Inc，2000:40-51.

[4]XU JIA，YAO YONG.Rationalizing Algorithm and Automated Proving for a Class of Inequalities Involving Radicals [J].Chinese Journal of Computers，2008，31(1):24-31(in Chinese).

[5]徐嘉.三角代數(shù)數(shù)極小多項(xiàng)式的機(jī)器求解[J].西南民族大學(xué)學(xué)報(bào):自然科學(xué)版，2012，38(3):439-443.

[6]YANG LU.Solving Harder Problems with Lesser Mathematics.Proceedings of the 10thAsian Technology Conference in Mathematics[C].ATCM Inc，2005:37-46.

[7]YANG LU，YAO YONG.Difference Substitution Matrices and Decision on Nonnegativity of Polynomials [J].Journal of Systems Science and Mathematical Science(in Chinese)，2009，29(9):1169-1177.

[8]XU JIA，YAO YONG.Polya’s Method and the Successive difference substitution Method ( in Chinese) [ J].Scientia sinica mathematica，2012，42(3):203-213.

[9]徐嘉.平面代數(shù)曲線的交點(diǎn)隔離算法[J].西南民族大學(xué)學(xué)報(bào):自然科學(xué)版，2015，41(5):614-620.

[10 ] BOTTEMA.Geometric Inequalities [ M].Groningen，Netherland: Wolters-Noordhoff Publishing，1969.

[11]LIUBAO QIAN.BOTTEMA，What we see[M].Lasha:Tibet People’s Publishing House，2003(in Chinese).

[12]KUANG JI CHANG.Applied Inequalities[M].3rded.Changsha:Hunan Educational Publishing House.2004(in Chinese).

[13]徐嘉，李高平.copositive二次型與copositive矩陣[J].西南民族大學(xué)學(xué)報(bào):自然科學(xué)版，2011，37(4):504-508.

(責(zé)任編輯：付強(qiáng)，張陽，李建忠，羅敏；英文編輯：周序林)

Rationalization and automated proving for three classes of inequalities involving radicals

XU Jia
(School of Computer Science and Technology，Southwest University for Nationalities，Chengdu 610041，P.R.C.)

Abstract:This paper studies rationalization and automated proving for three classes of inequalities involving radicals.Firstly，the sufficient and necessary conditions for deciding three types of radical inequalities are obtained.Then the adjoint polynomial on a simplex for a given polynomial is introduced.An algorithm SimplexM which can deal with polynomial inequalities with the conjunction∧(and)and∨(or)is established.Finally，some application examples confirm the effectiveness of this method.

Key words:inequality involving radicals;rationalization;automated proving

中圖分類號(hào)：TP301.6

文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：2095-4271(2016)02-0200-07

doi:10.11920/ xnmdzk.2016.02.013

收稿日期：2016-01-16

作者簡介：徐嘉(1981 - )，女，漢族，四川人，副教授，博士，研究方向:定理機(jī)器證明.

基金項(xiàng)目：國家民委資助項(xiàng)目(14XNZ023)，四川省教育廳創(chuàng)新團(tuán)隊(duì)(15TD0050)