[科普中国]-非退化条件

非退化条件(nondegenerate condition)是使几何命题不失一般性的条件。吴文俊最先明确指出：几何中一个有意义的定理，往往要附加若干限制条件，如平行四边形ABCD的对角线AC与BD互相平分，其限制条件是ABCD必须是非退化的平行四边形，即A，B，C，D四点不能在同一直线上。这样的限制条件就称为几何定理的非退化条件。

概念非退化条件(nondegenerate condition)是使几何命题不失一般性的条件。吴文俊最先明确指出：几何中一个有意义的定理，往往要附加若干限制条件，如平行四边形ABCD的对角线AC与BD互相平分，其限制条件是ABCD必须是非退化的平行四边形，即A，B，C，D四点不能在同一直线上。这样的限制条件就称为几何定理的非退化条件。

吴方法的精美处之一就是，整序过程中可以确定出一类非退化条件。具体地，从假设条件的多项式组经整序得到升列f1，f2，…，fs后，记fj的初式为Ij，则吴氏非退化条件为I1I2…Is≠0。当结论多项式g关于升列f1，f2，…，fs的余式为0时，升列f1，f2，…，fs的任一零点，只要满足非退化条件，就一定是g的零点。若不满足非退化条件，则可能不是g的零点。吴氏非退化条件另一应用是：若升列是由一多项式组PS整序而得到，则升列的零点满足非退化条件时，必为PS的零点。

使用格若勃基方法证明定理时，也会产生非退化条件——要求基的表达式中分母不为0。从同一多项式出发，所得到的吴氏非退化条件与格若勃基非退化条件不一定相同。1

弱非退化条件吴氏非退化条件的改进。由张景中、杨路等人提出.吴氏非退化条件要求升列中多项式初式不为0，即多项式关于主变元的最高次项系数不为0。弱非退化条件则只要求主变元各项系数不同时为0。例如，设

f1=x-u，f2=(x+2u)y-(3x+2u)y+(u+1)， g=u(2x+1)y-(3+2x)uy+x(u+1)。

欲判断在条件f1=f2=0之下是否有g=0，可按吴方法求g关于升列{f1，f2}的余式，结果余式为0。于是得到结论：在非退化条件x+2u≠0满足时，由f1=f2=0可得g=0。但由弱非退化条件，此结论可改进为：若(x+2u)，(3x+2u)，(u+1)不同时为0，则由f1=f2=0可得g=0。但又因(x+2u)，(3x+2u)，(u+1)显然不能同时为0，故得出结论“由f1=f2=0可得g=0”。2

人物简介吴文俊是数学家。上海人。1940年毕业于上海交通大学。1947年赴法国留学，先后在斯特拉斯堡、巴黎、法国科学研究中心进行数学研究，1951年获博士学位。1951年回国后，历任北京大学数学系教授，中国科学院数 学研究所研究员、副所长，中国科 学院系统科学研究所研究员、副所长、名誉所长、数学机械化研究中心 主任，中国数学会理事长，中国科学 院数学物理学部副主任，全国政协常务委员等职。1955年当选为中国 科学院物理学数学化学部委员。主 要从事拓扑学、机器证明学等方面的科学研究并取得多项突出成果， 是数学机械化研究的创始人之一， 为我国数学研究和科学事业的发展作出了重要贡献。1951年的博士论 文《球纤维空间示性类理论》是对纤 维空间基本问题的重要贡献。50年 代在示性类、示嵌类等研究方面取得了一系列突出成果，并有许多重 要应用，被国际数学界称为“吴文俊 公式”、“吴文俊示性类”，已被编入许多名著。这项成果获1956年国家 自然科学奖一等奖。60年代继续进 行示嵌类方面的研究，独创性地发 现了新的拓扑不变量，其中关于多 面体的嵌入和浸入方面的成果至今 仍居世界领先地位。在庞特雅金示 性类方面的成果，是拓扑学纤维丛 理论和微分流形的几何学的一项基 本理论研究，有深刻的理论意义。 近年来创立了定理机器证明的吴文俊原理(国际上称为吴氏方法)，实 现了初等几何与微分几何定理的机 器证明，达到了世界先进水平。这一重要创新改变了自动推理研究的面貌，在定理机器证明领域产生了 巨大影响，且有重要的应用价值， 它将引起数学研究方式的变革。这 方面的成果曾获全国科学大会重大 成果奖和中国科学院科技进步奖一 等奖。在机器发现和创造定理的研 究方面也已取得重要成果。发表研 究论文数十篇，并有专著多种。

格若勃基方法格若勃基方法是一种定理机器证明方法。是将格若勃基用于几何定理机器证明的方法.格若勃基方法已用于几百条几何定理的证明，并能从给定前提条件导出多种有几何意义的结论，以发现新定理.但在多数情形下，其效率不及吴方法.设要判定的命题已化为代数形式，假设条件可表示为：

hi(u1，u2，…，ud，x1，x2，…，xr)=0 (i=1，2，…，n)，

结论可表示为：g(u1，u2，…，ud，x1，x2，…，xr)=0。

格若勃基方法如下：

第一步：把x1，x2，…，xr看成变元，计算{h1，h2，…，hn}的格若勃基G，将g对G约化求出模G的正规形式。若其正规形式为0，则命题一般真(即在一组非退化条件下成立)。若不为0，则进行第二步。

第二步：引入新变量z，计算{h1，h2，…，hn，zg-1}的格若勃基。若此格若勃基为{1}，即仅含常数项——关于ui的多项式，则命题一般真。否则，命题不真。

在求取格若勃基的过程中，u1，u2，…，ud被看成参数，因而在格若勃基的表达式中，可能出现以u1，u2，…，ud为变元的分式。应用格若勃基证明定理时，要求这些分式的分母不为0。这也称为非退化条件。

机器证明计算机科学的重要研究方向之一，也是人工智能领域的重要组成部分。原意是用机械的步骤判定数学命题的真假，现在一般指用计算机证明定理或推导公式。根据不同要求，可以提出一理一证、一类一证或一般通用的机器证明方法。其形式又可以采用计算机辅助证明或计算机自动证明。

机器证明是数学机械化研究的一项重要内容。在计算机出现以前，这一领域已经走过了漫长的道路.17世纪，莱布尼茨(Leibniz，G.W.)和笛卡儿(Descartes，R.)分别从建立通用证明器和引进坐标、化一切问题为代数问题这两个角度，考虑了逻辑的和代数的机器证明问题。尽管当时的努力不足以取得明显的进展，却提出了有重大意义的研究方向。事实上，今天的机器证明理论，主要是沿着这两个方向发展和完善起来的。其中，希尔伯特(Hilbert，D.)、塔尔斯基(Tarski，A.)、贺布兰德(Herbrand，J.)和鲁宾孙(Robinson，J.A.)分别做出了重要的贡献.中国数学家吴文俊，从20世纪70年代后期开始致力于数学机械化及定理机器证明的研究，提出了一整套有效的、被国内外公认的吴方法或吴理论。吴理论本质上是采用代数方法研究机器证明.这一理论不但丰富了机器证明的内容，而且还带动了其他研究方法的发展.在吴理论的影响下，近年来还出现了GB法、例证法、数值并行法和可读性证明法等.这些方法的不断发展与完善，无疑具有重要的意义.机器证明就其方法而言是一些能判定某些命题真假的机械化方法，即一些算法.算法的作用域是由若干具有确定形式的命题组成的集。也就是说，算法工作开始时输入要检验的命题的前提与结论或只输入前提.算法工作结束时的输出可能有下列几种：

1.简单地断言命题成立或不成立，即输出命题的真值；

2.宣布算法对所输入的命题无效；

3.输出若干附加条件，并断言在这些附加条件下命题的结论成立；

4.输出证明的步骤；

5.输出由前提能推出的多种结论。

实际上，上述描述不能包罗机器证明的各式各样的描述与问题的提法，因为它是一个迅速发展而远未成熟的研究领域。3

本词条内容贡献者为:

尚华娟 - 副教授 - 上海财经大学