吴文俊
应当注意的是他在1956年前完成的研究成果的重要性,在多年以后才显现出来,至今仍在国际上广泛引用。
后期始于1976年,从事机器征明与数学机械化的研究。
他提出的用计算机证明几何定理的方法,与常用的基于数理逻辑的方法根本不同,显现了无比的优越性,改变了国际上自动推理研究的面貌,被称为自动推论领域的先驱性工作,并因此获得Herbrand自动推论杰出成就奖。以下是14届国际自动推论大会上对吴文俊工作的介绍与评价。
“吴文俊在自动推理界以他于1977年发明的(定理证明)方法著称。这一方法是几何定理自动证明领域的突破。”“几何定理自动证明首先由Herbert Gerlenter于五十年代开始研究。虽然得到了一些有意义的结果,但在吴方法出现之前的二十年里这一领域进展甚微。在不多的自动推理领域中,这种被动局面是由一个人完全扭转的。吴文俊很明显是这样一个人。”“吴的工作将几何定理证明自动推理的一个不太成功的领域变为最成功的领域之一。在很少的领域中,我们可以将机器证明归于一个人的工作。几何定理证明就是这样的一个领域。” 他引入的求解非线性代数方程组的吴方法是求解代数方程组精确解最完整的方法之一,已经被成功地用于解决很多问题,并实现在当前流行的符号计算软件中。欧共体资助的 POSSO计划(POlynomial System SOlving)中也有吴方法的专用软件包。吴方法还被用于若干高科技领域,得到一系列国际领先的成果。包括曲面造型,机器人机构的位置分析,智能CAD系统(计算机辅助设计),机器人,图像压缩等。 八十年代末,他提出了偏微分代数方程组的整序方法,是目前处理偏微分代数方程组的完整的构造性方法。该方法已被应用于微分几何定理机器证明和偏微分方程组求解。 扩展了代数簇的通常局限无奇点情形的陈示性数于有任意奇点的陈类与陈数,且定义是可计算的,形成代数几何机械化的新篇章。他给出了多元多项式组的零点结构定理,这是构造性代数几何发展的重要标志。
主要论著
1 Wu Wen-tsün. On the products of sphere bundles and the duality theorem modulo two. Ann of Math. , 1948, 49 (2): 641—653.2 Wu Wen-tsün. Sur les classes caracteristiques des structures fibrees spheriques. Actualites Sci. Ind. , No. 1183,Paris Hermann & Cie,1952.
3 吴文俊.Pontrjagin示性类,Ⅰ-V.数学学报,1953,3:291-315;1954,4:171-199;323-346;1955,5:37-63;401-410.
4 Wu Wen-tsün. A theory of imbedding, Immersion, and isotopy of polytopes in an Euclidean space. Beijing: Science Press, 1965. (中文本:吴文俊.可剖形在欧氏空间中的实现问题.北京:科学出版社,1978).
5 Wu Wen-tsiin. Rational homotopy type—a constructive study via the theory of the I-measure. Lecture Notes in Math. , No. 1264, SpringerVerlag, 1987.
6 Wu Wen-tsün. On Chern numbers of algebraic varieties with arbitrary singularities. Acta. Math. Sinica, New series, 1987, 3: 227—238.
7 吴文俊.我国古代测望之学重差理论评介,兼评数学史研究中某些方法问题.科技史文集第8辑.上海:上海科学技术出版社,1982:10-30.
8 吴文俊主编.《九章算术》与刘徽(中国数学史研究丛书之一).北京:北京师范大学出版社,1982.
9 吴文俊.出入相补原理.见8,第58-75页.
10 吴文俊.《海岛算经》古证探源.见8,第162-180页.
11 吴文俊主编.秦九韶与《数书九章》(中国数学史研究丛书之二).北京:北京师范大学出版社,1987.
12 吴文俊.从《数书九章》看中国传统数学构造性与机械化的特色.见11,第73-88页.
13 Wu Wen-tsün. Recent studies of the history of Chinese mathematics.(Proceedings of the international congress of mathematicians, Berkeley,California, USA, 1986) 1987, 1657—1667.
14 Wu Wen-tsün. On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica, 1978, 21: 159—172. (重印于 Automated Theorem Proving, after 25 years. W. W. Bledsoe & D. W. Lovelandeds. , 1984, 213—234.)
15 吴文俊.初等微分几何定理的机器证明.中国科学,数学专辑(Ⅰ),1979,94-102.
16 吴文俊.几何定理机器证明的基本原理(初等几何部分)(计算机科学丛书).北京:科学出版社,1984.
17 吴文俊主编.刘微数学讨论班报告集.合肥:安徽科学技术出版社,1988.
18 吴文俊.几何学机械化方法及其应用.见17,第181-188页.
19 Wu Wen-tsün. Mathematics-mechanization research No. 1—4. 1987—1996. (共收入吴文俊8篇论文,其中包括(1) A zero structure theorem for polynomial-equation solving,No. 1,pp. 2—12; (2)Mechanical