1997年吴文俊由于其在“几何自动推理领域的先驱性工作”被授予“Herbrand自动推理杰出成就奖”。该奖有国际自动推理学会颁发，用于奖励“对自动推理作出杰出贡献的个人或集体”。以前的获奖人包括自动推理创始人之一Larry Wos，自动推理创始人之一、前美国人工智能学会主席Woody Bledsoe，归结法的发明人Alan Robinson。 下面是对吴文俊先生获奖工作的介绍与评价。
1。 早在1982年，美国人工智能协会主席W. W. Bledsoe与两位McCarthy奖获得者R.S. Boyer, J.S. Moore联名致当时我国科技工作的领导人方毅，张劲夫和宋平，赞扬吴的工作是近十年中自动推理领域出现的最为激动人心的进展。信中认为：由于吴的工作，使中国的自动推理研究在国际上遥遥领先，并建议我国政府对这项研究给予充分的重视和积极支持。
2。自动推理核心刊物《自动推理杂志》全文转载吴的论文。编委J. C. Moore专门著文介绍吴的工作，认为吴的工作“不仅奠定了自动推理研究的基础，而且给出了衡量其它推理方法的明确标准”。
Distinguished Contributions to Automated Reasoning
Recipient: Professor Wu Wen-Tsun
The winner of this year's Herbrand Award,Professor Wu Wen-Tsun,is a member of the Academia Sinica,Beijing, and the founder of the Mechanized Mathematics Research Center of the Academia Sinica.
Wu is known in the automated deduction community for the method he formulated in 1977, marking a breakthrough in automated geometry theorem proving.
Geometry theorem proving was first studied in the 1950s by Herbert Gelernter and his associates. Although some interesting results were achieved, the field saw little progress for almost twenty years, until "Wu's method" was introduced. In few areas of automated deduction can one identify a specific person who turned the field around completely. Wu is clearly such a person. His work started from the observation of the (well-known) correspondence between plane geometry and analytic geometry. Specifically, one can transform a problem in elementary geometry into a set of polynomials and, by solving the polynomials, deduce the correctness of the theorem. This transformation of problems in geometry into problems in algebra enables researchers to use a full range of algebraic tools, which are much easier to automate than their counterparts in geometry. Wu based his method on Ritt's principle and a zero structure theorem for solving the polynomials. His method can be used not only to prove theorems in geometry, but also to discover theorems and to find degenerated cases automatically.
Wu started his research on geometry theorem proving in 1976, near the conclusion of the Cultural Revolution. He implemented his method on a rather primitive computer (the Great Wall 203 with 4K memory) in 1977 and proved the Simson line theorem. When visiting the United States for the first time in 1979, Wu acquired a more sophisticated computer (the HP9835A with 256K memory) and was able to prove more sophisticated problems such as the Morley theorem. S.C. Chou introduced Wu's method to the West while studying at the University of Texas in the early 1980s. Chou's prover proved several hundred theorems and further demonstrated the power of Wu's method. Geometry theorem proving was by then fully revised and became one of the most actively researched and successful areas in automated deduction.
Wu continued refining and extending his method and added a dazzling array of application domains whose proofs can be automated. They include plane geometry, algebraic differential geometry, non-Euclidean geometry, affine geometry and nonlinear geometry. Not limiting the applications to geometry alone, he also gave mechanical proofs of Newton's gravitational laws from Kepler's laws try theorem proving from one of the less successful research areas in automated deduction to one of the most successful. Indeed, there are few areas for which one can claim that machine proofs are superior to human proofs. Geometry theorem proving is such an area.
Born in Shanghai in 1919, Wu studied mathematics at the Shanghai Jiao-tung University. His education was interrupted for five years by the Sino-Japanese War. After the war. he enter the newly founded Institute of Mathematics of the Academia Sinica and resumed research in mathematics under S.S. Chern. In 1947, he went to the University of Strasbourg and studied topology under C. Ehresmann. After completing his state thesis in 1949 (on Grassmannian manifolds),he went to Paris and worked at the CNRS under E. Cartan. During his stay in France, Wu gained recognition for his work in topology. For instance, Cartan attributed the discovery of the Cartan formula to Wu. Wu also introduced what was later known as the Dold manifold.
After returning to China in 1951, Wu rejoined the Academia Sinica and continued to work in algebraic and differential topology until the Cultural Revolution. He made important contributions to the theory of Euclidean spaces and Pontrjagin theory, among other areas. he also turned the important "rational homotopy theory" created by D. Sullivan into algorithmic form, introducing a new terminology called I*-functors. Indeed, Wu's contributions to topology are no less significant than those to automated deduction.
The third area to which Wu made important contributions is the history of Chinese mathematics. His studies initiated from an ancient classic Nine Chapters of Arithmetic (dated about 100 B.C.) and its Annotations by Liu Hui (in A.D. 263). Liu also extended an ancient method for calculating the height of the sun, which apeared in the ancient script Zhoupi Suanjing (The Calculus of Zhoupi), to a general algorithm for calculating height, called Chongchashu (Double-Difference Algorithm). Liu's results were stated without explanations (or, more precisely, the explanations were lost) and were included in his work Haidau Suanjing ( the Calculus of Islands). Wu compared the various scripts and reconstructed the proofs of Liu's theorem in an ancient style, quite different from the usual Euclidean approach. He further argued that Chinese mathematics has its own tradition, which is based on computation as opposed to the axiomatic and proof approach of Western mathematics. To some extent, Wu's own work on geometry theorem proving is a demonstration of how East meets West and how the two trends of thought complement each other.