初等几何定理机器证明——吴方法简介，本文主要内容关键词为：定理论文,几何论文,机器论文,简介论文,吴方论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
吴文俊院士获得2000年国家科学技术最高奖，这对我们数学工作者是极大的鼓舞，他的主要成就包括代数拓扑，应用数学，数学史，几何定理的机器证明等。这里，我们介绍后者。
1 数学的特征与它的机械化问题
1.1 数学的基本特征
数学中既有结构，也有计算。数学中的结构表现在多方面，例如实数的有序性，就具有“序”的结构；计算与算法的例子也很多，例如解线性方程组的“九章—秦九韶—高斯消元法”。应该指出，结构与算法不是对立的。与两个基本特征相应，从数学研究的方法论的角度来看有公理化方法，其代表作：欧几里德的《几何原本》；上世纪希尔伯特的《几何基础》问世，进一步发展与完善了公理化方法。另一方面还有算法化（或构造性）方法，它的代表作在东方（中国）有《九章算术》。
1.2 数学的机械化
什么是数学的机械化？考察人们的体力劳动，很多是机械性的动作，在工业革命之后，设计各种机器，实现体力劳动机械化。数学的学习与研究是典型的脑力劳动之一，它能否部分实现机械化？数学问题的机械化，就是要求在运算或证明过程中，每前进一步之后，都有一个确定的，必须选择的下一步，这样沿着一条有规律的，刻板的道路，一直达到结论。算法化方法的发展，导致了算法概念的精确化，这为计算机的诞生创造了条件。现代电子计算机的出现，反过来又直接促进数学的繁荣与发展。
2 吴方法
2.1 机器证明定理历史简述
几何定理的机器证明，自1945年出现了第一台电子计算机之后更是激起人们的关注。1948年，波兰人Tarski解决实闭域初等几何定理可以机械化的证明（见A.塔尔斯基，J.C.C.麦克铿，初等代数和几何的判定法。北京：科学出版社，1959，陆钟万译）用的是数理逻辑法，虽然也给出实现这些证明的建议，但离实现非常遥远，并非切实可行。
1956年之后美国开始利用电子计算机做证明定理的尝试。
1959年，王浩设计一种方法，用计算机证明了罗素的《数学原理》中几百条定理，仅用9分钟，引起轰动， 一时机器证明前景似乎非常乐观，当时人们猜测再过十年计算机将证明发现新定理，然而实践上人们碰到困难，1976年美国做了大量实验，塔尔斯基的初等几何，用计算机证明一些近于同义反复的“儿戏”式的“定理”，例如“若P[,1]，P[,2]，P[,3]，P[,4]，P[,5]五个点之中，P[,1]，P[,2]，P[,3]和P[,1]，P[,2]，P[,4]和P[,1]，P[,2]，P[,5]各在一条直线上，则P[,3]，P[,4]，P[,5]也在一条直线上”。 （见Kister，K.IEEE Trans on ComputersC—25（1976），328—334）。于是人们又走向悲观的一面，有些专家估计：靠机器再过100年， 也未必能证明出多少有意义的新定理。
如前所述初等几何和初等代数的判定问题早在50年代就为塔尔斯基（A.Tarski）所解决，但其复杂度远远超越了现代计算机的能力范围。总之，几何定理由计算机自动地证明，于20世纪五十年代由赫伯特格兰特（Herbert Gerlenter）开始研究。虽然也取得一些有意义的结果，当时经过20多年的努力，到了二十世纪七十年代，进展甚微。具有实际意义的，在自动推理领域先驱性的工作，是由数学机械化思想的倡导者吴文俊院士于70年代作出的，这就是著名的几何定理机器证明的吴氏方法，是第一个可以证明非平凡定理的系统的机器证明方法。他将几何定理证明从一个不太成功的领域，变为最成功的领域之一。
2.2 吴方法简述
吴方法主要分两步。
第一步是引进坐标，然后把需证定理中的已知条件与结论部分都用坐标间的代数关系来表示。我们所考虑的初等几何定理局限于这
