吴消元法

吴消元法，又称吴特征列方法，是吴文俊院士创立的将多元多项式方程组简化然后求解的机械化算法。吴消元法可用计算机实现，是数学机械化的基础。

多项式的指标

多项式：

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