机器证明的回顾与展望-httpwwwcqvipcom.pdf

{匙理兹稍)／徽程

第16卷第5g期大自然探索VoIl16，SumNo．；9
1997年第1期EXPLORAT10NOFNATURENo．1，】997
6厂70}铂一≯
机器证明的回顾与展望
嗍
辜中国科学院成都计鼽算机应用研究所研究言员堡二壹—／

机器证明及其应用．是我国攀登计划项目之一。项目核心内容主要是几何定理机器证明和
非线性代数方程组理论、算法和应用实际上．机器证明研究领域的范围要广泛得多。在国外

由于传统的兴趣和多种原因．几何定理的机器证明在自动推理的研究中占有重要的地位。
近二十年来，几何定理机器证明的研究和实践有了很大的进展。

1从古老的梦想到惊人的突破

能否建立一个通用的几何解题方法．成批地解决问题，以至万理一证．是历史上一些卓
越的科学家的梦想
为此，笛卡尔发明了坐标系；莱布尼兹设想过推理机器；希承伯特在其名著《几阿基
础》中给出了一类几何命题的i堕j童理电乇土算机橄的出现推动了数学机械化。50年代·塔
斯基用代数方法证明了初等几何的机械化的可能性到60年代，斯拉格和莫色斯实现了符号积
分．代数与分析计算问题的机械化已经初具规模，而几何定理的机器证明看来仍遥遥无期。接
着．格兰特等提出用逻辑方法建立几何推理机．科林斯等改进了塔斯基的代数方法。直到1975
年，仍找不到能用计算机判定非平凡几何命题的有效算法。正当这一领域的热情由于进展缓慢
而趋于冷落之际．吴文俊方法(吴法)的提出，给定理机器证明的研究带来勃勃生机。用吴
法可在微机上很快地证明困难的几何定理。周成青发展了吴浩并把它实现为有效的通用程序．
证明了5】2条非平凡定理，写成英文专著。这一进展是自动推理领域一大突破，被国际国行誉
为革命性的工作。

2从机器判定到可读证明的自动生成

吴法的成功使一度冷落的凡便定理机器证明研究活跃起来用代数方法证明几何定理的
方向受到重视新的代数方法接连出现在国外．周成青等提出了用Grobner基方法构作几何
定理机器证明的算法和程序并得到成功。在国内，洪家威提出了单点例证方法的理论设想．

·6·
●

f

——～一—．————，L

夫自然探索1997年第l期(包第59期)

但因复杂度太大不能实现]。张景中、扬路则提出数值并行方法，在低挡微机(甚至计算器)上
实现了非平凡几何定理的机器证明和机器发明]。数值并行方法的优点是所需内存极少，且
易于并行化。所有这些方法都属于代数方法。它们的提出和实现丰富了几何定理机器证明的研
究。但与吴法相比．没有大的新突破。
代数方法不能使人满意的是，它所给出的“证明”是关于大多项式的繁复的计算．人难
于理解其几何意义，也难于检验其是否正确能否让计算机生成人能理解和易于检验的简明巧
妙的证明，所谓可读证明，是对自动推理和人工智能领域的一个挑战性的课题。一些著名的科
学家认为，机器证明的基本思想是量的复杂取代质的困难，这就很难想象用机器生可读证
明。国外一些学者从6O年代即致力于几何定理可读证明自动生成的研究，三十多年来进展不
大．未能给出哪怕是一小类非平凡几何定理的机器证明的有效算法和程序。
作者以他多年来所发展的几何新方法为基本工具．并提出了消点思想，和周成青、高小
山合作，于1992年突破了这一困难，实现了几何定理可读证明的自动生成=，这一新方法既不
以坐标为基础，也不同于传统的练合方法，而是一个以几何不变量为工具．把几何、代数、逻
辑和人工智能方法结合起来所形成的开放系统。它选择几个基本的几何不变量和一套作图规
则，并且建立一系列与这些不变量和作图规则有关的消点公式。当命题的前提以作图语句的形
式输入时，程序可调用适当的消点公式把结论中的约束点逐个消击．最后达到水落石出。消点
的过程纪录与消点公式相结合+就是一个具有几何意义的证明。此算法对可构造等式型几何命
题是完全的，但其应用范围不限于这一类命题。基于此法所编的程序，已在微机上对数以百计
的困难的几何定理完全自动地生成了简短的可读证明，其效率也比其他方法为高。随所用的几
何量的不同，它能生成面积法、向量法、复数法和全角法等多种风格的证明，也能用于立体
几何。杨路、高小山、周咸青与作者合作，把消点法用于非欧几何可读证明的自动生成也得到
成功，并得到一批非欧几何新定理。消点法也可用于几何计算和公式推导。基于几何量和消点
思想的新原理的建立，像是打开了几何定理机器求解的一个矿床。它也使几何定理机器证明的
成果在数学教育中的应用有了现实可能。这一成果被国际同行誉为使计算机能像处理算术那
样处理几何的发展道路上的里程碑，是自动推理领域三十年来最重要的工作。
在多数情形下，消点法也可用笔纸证明不平凡的定理。它结束了2000年来几何证题无定法
的局面，把初等几何解题法从四则杂题的层次推进到代数方程的阶段