差分代換與不等式機(jī)器證明

1、 6 廣州大學(xué)學(xué)報(bào) ( 自然科學(xué)版 3 3 第 5卷 3 2 然如此 , 各變元的量綱應(yīng)該是相同的. 即所處理的 多項(xiàng)式應(yīng)該是齊次的. 雖然 SDS 程序?qū)Ψ驱R次的 多項(xiàng)式也能運(yùn)用 , 但效果不佳. 所以如果遇到非齊 次的多 項(xiàng) 式, 建 議 先 將 其 齊 次 化 , 然 后 再 執(zhí) 行 SDS. g5 = x 1 (x 2 + x 3 + x 4 + x 2 (x 1 + x 3 + x 4 + x 3 (x 1 + x 2 + x 4 + x 4 ( x 1 + x 2 + x 3 - 2x 1 ( x 2 + x 3 + x 4 2x 2 ( x 3 + x 4 - 2x 3 x 4

2、都是 4 元 4 次半正定對(duì)稱形式 . 定理 3 一個(gè) 3 元 5 次對(duì)稱形式 F (x, y, z 滿 足條件 F ( 1, 1 , 1 = 0 , 那么 F 是差分代換平凡的 , 當(dāng)且僅當(dāng)存在 8 個(gè)非負(fù)實(shí)數(shù) b1, b2, , b8 使得 F = b1 f1 + b 2f 2 + + b 8f 8 4 4 2 2 2 2 2 3 2 2 2 3 關(guān)于對(duì)稱形式 本文討論了一種試探性的方法 , 而不是一種 完備的算法. 迄今我們還不能 夠較好地界定 SDS 所能處理的多項(xiàng)式的范圍 . 這方面的研究還有待 去做. 下面將不加證 明地?cái)⑹鰩讉€(gè)關(guān)于對(duì)稱形式 ( 即對(duì)稱齊次多項(xiàng)式 的結(jié)果. 一個(gè)形式

3、 F 叫做是 差分代換平凡 的 , 如果 集合 DS (F 是平凡非負(fù)的. 定理 1 一個(gè) 3 次對(duì)稱形式 f ( x 1, x 2, 滿足條件 f ( 1 , 1 , n + ( 20 其中 f1 = x + y + z - x (y + z - y (x + z - z (x + y + xyz( x + y + z , f2 = x ( y + z + y (x + z + z (x + y - x ( y + z y (x + z - z ( x + y - 2xyz ( x + y + z + 2xyz (xy + yz + xz , f3 = x (y + z + y ( x +

4、z + z ( x + y 2xyz (x + y + z , f4 = x yz + xy z + xyz - x y z - xy z - x yz , f5 = x + y + z - 2x y - 2x z - 2y x - 2y z - 2z x 2z y + x y + x z + y x + y z + z x + z y + 4x yz + 4xy z + 4xyz - 3x y z - 3xy z - 3x yz , 4 4 4 4 4 4 3 3 f6 = x y + x z + y x + y z + z x + z y - 8x yz - 8xy z 8xyz + 6x

5、 y z + 6xy z + 6x yz , f7 = 2x + 2y + 2z - 5x y - 5x z - 5y x - 5 y z - 5z x 5z y + 3x y + 3x z + 3y x + 3y z + 3z x + 3z y + 14x yz + 14xy z + 14xyz - 12x y z 12xy z - 12x yz , f8 = 3x ( y + z + 3y ( x + z + 3z ( x + y - 2x ( y + z - 2y (x + z - 2z (x + y - 14xyz( x + 2 3 2 2 3 2 2 2 4 4 4 3 2 2 2

6、2 2 3 2 3 3 3 2 2 4 3 2 3 2 3 2 3 2 3 2 5 5 5 4 4 4 4 4 3 2 2 2 2 2 2 3 3 3 2 2 2 2 2 2 4 3 2 3 2 3 2 3 2 3 2 3 2 5 5 5 4 4 4 4 4 3 3 3 2 2 2 2 2 2 2 2 2 3 2 2 3 2 2 3 2 2 3 2 2 3 2 2 2 2 2 4 4 4 3 2 2 2 2 2 5 5 5 4 , xn , 1 = 0 , 那么 f 在 R 上是半正 定的當(dāng)且僅當(dāng)它是差分代換平凡的. 定理 2 一個(gè) 4 元 4 次對(duì)稱形式 G ( x 1, x 2, x 3,

7、 x 4 滿足條件 G ( 1 , 1 , 1, 1 = 0 , 那么 G 是差分代換 平凡的 , 當(dāng)且僅當(dāng)存在 5個(gè)非負(fù)實(shí)數(shù) a1, a 2, a3, a4, a5 使得 G = a 1g 1 + a2 g 2 + a3 g 3 + a 4g 4 + a5 g5, 其中 g 1 = 3x + 3x + 3x + 3x - 4x (x 2 + x 3 + x 4 4x 2 ( x 1 + x 3 + x 4 - 4x 3 (x 1 + x 2 + x 4 - 4x 4 (x 1 + x 2 + x 3 + 2x 1 (x 2 + x 3 + x 4 + 2x 2 ( x 3 + x 4 + 2

8、x 3x 4 + 4x 1 ( x 2 x 3 + x 3 x 4 + x 2 x 4 + 4x 2 ( x 1x 3 + x 3 x 4 + x 4x 1 + 4x 3 ( x 1 x 2 + x 2 x 4 + x 4 x 1 + 4x 4 (x 1x 2 + x 2x 3 + x 1 x 3 - 24x 1x 2 x 3 x 4, g 2 = x 1 (x 2 + x 3 + x 4 + x 2 ( x 3 + x 4 + x 3x 4 - x 1 (x 2 x 3 + x 3 x 4 + x 2x 4 - x 2 (x 1x 3 + x 3x 4 + x 4 x 1 - x 3 (x

9、1 x 2 + x 2 x 4 + x 4x 1 - x ( x 1 x 2 + x 2x 3 + x 1 x 3 + 6x 1x 2 x 3 x 4, g 3 = 3x 1 + 3x 2 + 3x 3 + 3x 4 - 2x 1 (x 2 + x 3 + x 4 2x 2 ( x 1 + x 3 + x 4 - 2x 3 (x 1 + x 2 + x 4 - 2x 4 (x 1 + x 2 + x 3 - 2x 1 (x 2 + x 3 + x 4 - 2x 2 ( x 3 + x 4 2x 3x 4 + 3x 1 ( x 2 x 3 + x 3 x 4 + x 2 x 4 + 3x 2 (

10、 x 1x 3 + x 3 x 4 + x 4x 1 + 3x 3 ( x 1 x 2 + x 2 x 4 + x 4 x 1 + 3x 4 (x 1x 2 + x 2x 3 + x 1 x 3 - 12x 1x 2 x 3 x 4, g 4 = x 1 (x 2 x 3 + x 3x 4 + x 2 x 4 + x 2 (x 1x 3 + x 3 x4 + x 4x 1 + x (x 1 x 2 + x 2x 4 + x 4x 1 + x ( x 1 x 2 + x 2 x 3 + x 1 x 3 - 12x 1 x 2 x 3x 4, 2 3 2 4 2 2 2 2 2 2 2 2 2 2

11、 2 2 2 2 2 3 3 3 4 4 4 4 3 2 4 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3 3 4 1 4 2 4 3 4 4 3 1 y + z + 12xyz( xy + yz + xz 都是 3元 5次半正定對(duì)稱形式. 諸如此類的結(jié)果就 不多列舉了 . 2 2 4 結(jié)束語 基于一種最初可能是起源于無名氏的樸素思 想, 我們設(shè)計(jì)了一個(gè)試探性的程序用于證明多項(xiàng)式 不等式, 或等價(jià)地, 用于判定多項(xiàng)式的非負(fù)性. 那就 是, 將各變量按一定方式分割成較小的非負(fù)量, 將 變量替換后的多項(xiàng)式合并同類項(xiàng), 然后看是否所有 的

12、系數(shù)都是非負(fù)的. 過去這方法常見于某些對(duì)稱形 式的不等式的證明, 沒有考慮怎樣應(yīng)用于非對(duì)稱情 形, 也未考慮如果一次不成, 能否再接再厲. 本程序 第 2期 楊 路 : 差分代換與不等式機(jī)器證明 7 針對(duì)這兩點(diǎn)作了發(fā)展. 雖然有關(guān)的理論探討剛剛開 始, 但許多實(shí)驗(yàn)結(jié)果表明該程序?qū)Σ簧俣囗?xiàng)式是很 有效的. 現(xiàn)今國內(nèi)外提供了不少做 實(shí)代數(shù) 的軟件包, 如 REDLOG , QEPCAD , BOTTEMA 5 2 3 4 動(dòng)地 證明不等式, 但除了新版的 bottem a( 它含有 子程序 SDS 其余都不能證明變量較多、 次數(shù)較高 的多項(xiàng)式不等式, 如問題 7 . 此外, 差分代換的方法和程序只

13、用到不多的數(shù) 學(xué), 容易被讀者理解和接受 認(rèn)為是 可讀 的 . 6 及 D IS . 其產(chǎn)生的證明可以 COVERER 等多種 . 它們都能夠在某種程度上 自 參考文獻(xiàn): 1 2 3 4 5 6 R ezn ick B. Some concrete aspects of H ilbert s 17th prob le m, Co m tempo rary M athe m atics , V o.l 253M . Am erican M athe m atica l Society , Prov idence , RI , 2000: 251 272 . Do lzman A, Stur m

14、T. REDLOG: Computer a lgebra meets co mputer log ic J. ACM SIGSAM Bu lletin, 1997, 31( 2: 2 9. Co llins G E, Hong H. Partial cylindr ica l a lgebra ic decompo sition fo r quantifier eli m ination J. Journal of Sy mbo lic Co m puta tion, 1991, 12 : 299 328 . Y ang L , Zhang J . A practica l progra m

15、of auto m ated prov ing for a c lass of geo m etr ic inequa litiesM in G eo m etry , Lecture N otes in A rtific ia l Inte lligence 2061 . Berlin: Spr inger V erlag , 2001 : 41 57 . Y ang L , H ou X R, X ia B C. A co m plete a lgor ithm of auto m ated d iscovering fo r a class of inequality type theo

16、 rems J. Sci ence in Ch ina F , 2001 , 44: 33 49. Y ang L . Solv ing H arder Prob le m sw ith LesserM athe m atics C /P roceed ings o f the 10th A sian T echno logy Conference in M a th e m atics , B lacksburg : ATCM Inc , 2005: 37 46. A uto m ated D educ tion D ifference substitution and auto mated

17、 inequality proving YANG L u ( Inst itu te for E du cat ional Softw ares , G uangzhou U n ivers ity, G uangzhou 510006 , Ch ina Abstract : A progra m nam ed SDS is designed for po lynom ial inequality prov ing, in other w ords , fo r decision of nonnegat iv ity of po lynom ia ls . The basic idea is

18、: split the variab les in to sm aller nonnegat iv e quantities, then , co l lect the ter m s and see whether the coefficients all are nonnegat iv e . T he m ethod has been used to prove symm etric polyno m ia l inequalit ies for so m any years th at th e orig in is unava ilab le . T his is a heuristic , not a com plete alg o rithm. H ow ever , it w as de m onstr