吴文俊传_吴文俊方法(Wu Wenjun method)一种定理机器证.doc

最新吴文俊传_吴文俊方法(Wu Wenjun method)一种定理机器证吴文俊方法吴文俊吴文俊方法一种定理机器证明方法.是由吴文俊创立并加以系统化和完善的定理机器证明方法简称吴方法.吴方法以构造性的代数几何理论为工具将几何定理的求证问题经坐标化和代数化之后转变成判定两个代数簇的有条件的包含关系再加以解决.应用吴方法建立的程序系统已经证明了数百条高难度的几何定理同时还发明了若干新定理.吴方法还可用于证明非欧氏几何中的定理并能证明若干微分几何定理及解决微分方程中的某些定性问题. 用吴方法判定一个命题其本质是判定一组多项式的公共零点集是否被包含于另一多项式的零点集的问题.分三步进行:第一步是把所给命题化为代数形式.第二步是整序即把刻画命题条件的多项式组PS经整序化为升列AS.第三步是求余即将刻画命题结论的多项式g对升列AS约化求余式R. 若R为即可断定命题在非退化条件I1IZ ...1k并吴文俊之下成立或者说命题一般成立.其中111:…I*是升列AS中各多项式的初式之积.若R不为0则当AS为不可约升列时可断定命题不真.吴文俊方法(Wu Wenjun method)一种定理机器证明方法.是由吴文俊创立并加以系统化和完善的定理机器证明方法，简称吴方法.吴方法以构造性的代数几何理论为工具，将几何定理的求证问题，经坐标化和代数化之后，转变成判定两个代数簇的有条件的包含关系，再加以解决.应用吴方法建立的程序系统已经证明了数百条高难度的几何定理，同时还发明了若干新定理.吴方法还可用于证明非欧氏几何中的定理，并能证明若干微分几何定理，及解决微分方程中的某些定性问题. 用吴方法判定一个命题，其本质是判定一组多项式的公共零点集是否被包含于另一多项式的零点集的问题.分三步进行:第一步是把所给命题化为代数形式.第二步是整序，即把刻画命题条件的多项式组PS经整序化为升列AS.第三步是求余，即将刻画命题结论的多项式g对升列AS约化求余式R. 若R为。

即可断定命题在非退化条件I1IZ ...1k并之下成立，或者说命题一般成立.其中111:…I*是升列AS中各多项式的初式之积.若R不为0，则当AS为不可约升列时，可断定命题不真.推荐访问: 第 2 页 共 2 页。