摘要
机器证明的思想可以回溯到 17世纪的 Descartes与 Leibnize,2 0世纪初 Hilbert更明确地提出了公理系统的机械化判定问题。但是 ,随后的种种努力都未能使机器证明取得本质的进展。近 2 0年来 ,吴文俊继承并发展了中国古代的数学思想 ,在定理机器证明上开创了以多项式组零点集为基本点的消元方法 ;吴文俊的数学机械化方法已在物理规律的发现、机器人学、计算机视觉以及促进现代数学研究等重大高科技的前沿领域实现了成功的应用。数学机械化研究的兴起 。
The idea of proving theorems mechanically may be dated back to Descartes and Leibnize in the 17th century and has been formulated in precise mathematical forms in the 20th century through the school of Hilbert. In spite of vigorous efforts, however, researches in this direction give rise quite often to negative results. For example, the methods of Tarski based on a generalization of Sturm are still too complicated to be feasible, even with the use of computers. It is Wu Wen-tsun who established a new algorithm for the mechanization of theorem-proving in elementary geometry. Wu's methods were all originated and quite developed from ancient Chinese mathematics. In fact, the algebrization of geometrical problems and systematic method of their solution by algebraic tools were some of the main achievements of classical Chinese mathematics. Now, the method of mathematical mechanization has been played an important role in mathematics, and gotten its wide applications.
出处
《上海交通大学学报（哲学社会科学版）》
2001年第3期13-18,共6页
Journal of Shanghai Jiao tong University(Philosophy and Social Sciences)
关键词
数学机械化
中国
古代数学
吴文俊
《九童算术》
mechanical proving
mathematics mechanization
classical Chinese mathematics
Wu Wen-tsun
