初等几何定理机器证明.pdfVIP

2001 年第 11 期 　　　　　　　　　　　　　数 学 通 讯 1 初 等 几 何 定 理 机 器 证 明 ———吴方法简介 梁 肇 军 (华中师范大学数学系, 武汉 　430079) ( ) 中图分类号:O123 - 39 　　　　文献标识码 :C 　　　　文章编号 :0488 - 7395 2001 11 - 0001 - 02 　　吴文俊院士获得 2000 年国家科学技术最高奖, 电子计算机之后更是激起人们的关注. 1948 年, 波兰 这对我们数学工作者是极大的鼓舞, 他的主要成就 人 Tarski 解决实闭域初等几何定理可以机械化的证 ( 包括代数拓扑, 应用数学, 数学史, 几何定理的机器 明 见 A . 塔尔斯基, J . C. C. 麦克铿, 初等代数和几 ) 证明等. 这里, 我们介绍后者. 何的判定法. 北京 :科学出版社, 1959, 陆钟万译 用 1 　数学的特征与它的机械化问题 　 的是数理逻辑法, 虽然也给出实现这些证明的建议, 1. 1 　数学的基本特征 　 但离实现非常遥远, 并非切实可行. 数学中既有结构, 也有计算. 数学中的结构表现 1956 年之后美国开始利用电子计算机做证明定 在多方面, 例如实数的有序性, 就具有“序”的结构; 理的尝试. 计算与算法的例子也很多, 例如解线性方程组的“九 1959 年, 王浩设计一种方法, 用计算机证明了罗 章 —秦九韶 —高斯消元法”. 应该指出, 结构与算法 素的《数学原理》中几百条定理, 仅用 9 分钟, 引起轰 不是对立的. 与两个基本特征相应, 从数学研究的方 动, 一时机器证明前景似乎非常乐观. 当时人们猜测 法论的角度来看有公理化方法, 其代表作 :欧几里德 再过十年计算机将证明发现新定理. 然而实践上人 的《几何原本》; 上世纪希尔伯特的《几何基础》问世, 们碰到困难, 1976 年美国做了大量实验, 塔尔斯基的 进一步发展与完善了公理化方法. 另一方面还有算 初等几何, 用计算机证明一些近于同义反复的“儿 ( ) ( ) 法化 或构造性 方法, 它的代表作在东方 中国 有 戏”式的“定理”, 例如“若 P1 , P2 , P3 , P4 , P5 五个点 《九章算术》. 之中, P1 , P2 , P3 和 P1 , P2 , P4 和 P1 , P2 , P5 各在一 1. 2 　数学的机械化 　 条直线上, 则 P3 , P4 , P5 也在一条直线上”. (见 Kist 什么是数学的机械化 ? 考察人们的体力劳动, er , K. IEEE Trans on Computers C - 25 ( 1976