吳消去法

吳消去法，又稱吳特徵列方法，是吳文俊院士創立的將多元多項式方程組簡化然後求解的機械化算法。吳消去法可用計算機實現，是數學機械化的基礎。

多項式的指標

多項式：

P=P($x_{1}$,$x_{2}$,……$x_{n}$)中

主變元

變元($x_{1}$,$x_{2}$,……$x_{n}$)中下標最大下標

稱為多項式P的主變元，記為 Ivar(P)

例如 P=$-2*x_{2}^{2}-x_{1}*x_{2}^{2}+2*x_{1}*x_{2}+2*x_{1}^{2}*x_{1}+x_{1}^{3}$

變元為$x_{1}$,$x_{2}$,主變元為 Ivar(P)$=x_{2}$。

多項式的類

多項式P的類定義為 主變元 Ivar(P)的下標，記作 cls(P).

上例多項式P的類 為 cls(P)=2。

多項式的次數

多項式關於變元$x_{i}$的次數 記為 deg(P,$x_{i}$)

多項式關於主變元的次數，記為deg(P)=deg(P,ivar(P))

多項式的長度，定義為多項式的項數，記為 t(P).

多項式的指標集[t(P),cls(P),deg(P)]。

多項式的初式和正則形式

初式

多項式的初式，是多項式主變數最高冪項的係數，記為 init(P)

例如 P=$-2*x_{2}^{2}-x_{1}*x_{2}^{2}+2*x_{1}*x_{2}+2*x_{1}^{2}*x_{1}+x_{1}^{3}$

$=(-2-x_{1})*x_{2}^{2}+2*x_{1}*x_{2}+2*x_{1}^{2}*x_{1}+x_{1}^{3}$

init(P)=$(-x_{1}-2)$;

初式 init(P)是一個除主變元之外的多項式I

：I=I($x_{1}$,$x_{2}$,……$x_{c-1}$)

其中 c=cls(P) 是多項式 P的類。

正則形式

將多項式表示為

P=$I*x_{c}^{d}+$關於$x_{c}$的低次冪項，稱為多項式P的正則形式。

多項式的偏序和約化

P，Q為非零多項式，如果 cls(P)<cls(Q)，或cls(P)=cls(Q)，但deg(P)<deg(Q),則稱P的序低於Q的序。記為 P<Q。

如果P<Q，或Q< P 都不成立，則P，Q同序，記為 P~Q.

約化

多項式 P，Q，如果

cls(P) =c>0； deg(Q,$x_{c}$)<deg(P).

則稱P對於Q是約化的

如果多項式P的初式 init(P) 是常數，則對於任何低類多項式Q，（cls(Q)<cls(P))都是約化的。

例子：

P=$(x_{1}+3)*(x_{1}+8)*x_{2}^{5}+S(x_{1},x_{2})$

Q=$(x_{1}+1)*(x_{1}+2)*(x_{1}+3)*x_{2}^{2}$

其中 ivar(P)=$x_{2}$

cls(P)=c=2

deg(P)=5

deg(S)<5

deg(Q,$x_{c}$)=2;

P 對於 Q 是約化的。

升列與三角列

升列

多項式集 AS: $A_{1}$,$A_{2}$....$A_{r}$是一個升列

如果滿足以下兩個條件：

1. cls($A_{1}$） < cls($A_{2}$) <....< cls($A_{r}$)
2. init($A_{j}$) 關於 $A_{i}$ 對於任意的 i<j 是約化的。

三角列

如果非零多項式集 AS: $A_{1}$,$A_{2}$....$A_{r}$

只滿足：

cls($A_{1}$） < cls($A_{2}$) <....< cls($A_{r}$)

則非零多項式集 AS 是一個三角列，又稱為弱升列。

多項式求餘與零點集

兩個多項式:F,G, 其中 cls(F)=c,init(F)=I,通過多項式除法可得：

$I^{s}*G=Q*F+R$

如取s儘量小，R稱為 G關於F的Ritt餘式，記為 R=Remdr(G/F)

零點集

多項式方程組 PS =0 的全部解，稱為PS 的零點集，記為 Zero(PS)

兩個多項式方程組 $P_{1}$,$P_{2}$

如果 R=Remdr($P_{2}$/$P_{1}$)

則 Zero(PS)=Zero($P_{2}$,$P_{1}$)=Zero(($P_{2}$,$P_{1}$,R)

加入餘式，零點集不變。

多項式對升列的餘式

給出一個多項式P=P($x_{1}$,$x_{2}$……$x_{k}$}和一個升列 AS={$A_{1}$,$A_{2}$……$A_{k}$}

按反向次序連環計算下列餘式：

$r_{k}$=Remdr(P / $A_{k}$)

$r_{k-1}$=Remdr($r_{k}$ / $A_{k-1}$)

$\ldots$

$r_{1}$=Remdr($r_{2}$ / $A_{1}$)

最後得到的餘式 $r_{1}$≡R≡Remdr(P/AS) 稱為 P 對於 AS 的餘式。

R 是唯一確定的多項式。

R 對於 AS 是約化的。

軟體包

• 王東明 以 Maple 編寫的 CharSets 軟體包，自1991年就成為Maple Shared Library 的軟體包，也是他2003年 Epsilon Maple軟體包的組成單元之一
• 數學機械化自動推理平台 MMP 3.0 有 charser 軟體，但MMP 3.0 平台為半成品，用戶寥寥無幾，遠不如 王東明 CharSets 軟體包成功。

應用

• 計算機視覺、自動化定理證明、機器人、生物

參考文獻

書籍

• 吳文俊 著 《數學機械化》 科學出版社 2006 ISBN 7-03-010764-0
• Wen-tsün Wu, The Characteristic Set Method and Its Applications, p4-41 Mathematics Mechanization and Applications, Ed, Xiao-Shan Gao, Dongming Wang, Academic Press 2000 ISBN 0-12-734760-7
• 王東明 著 《消去法及其應用》 科學出版社 2002 ISBN 7-03-010560-5
• Dongming Wang（王東明）. Elimination Practice London: Imperial College Press, 2004, ISBN 1-86094-438-8
• 高小山、王定康、裘宗燕、楊宏 著 《方程式求解與機器證明》 科學出版社 2008 ISBN 978-03-017862-6
• 關靄雯 編 《吳消去法講義》 北京理工大學 1994