计算机能证明定理吗

在学习数学课程时，大家都碰到过“定理证明”的问题。定理证明可以说是一种最典型的逻辑推理过程。

长期以来，人们一直在寻找自动证明定理的方法，希望有一天，向计算机输入一个待证的数学定理，运行计算机里的定理证明系统，很快就得到定理的证明。

自动定理证明亦称为“机器证明”。

计算机之所以能证明定理，是因为专家们先将一些公理和规则符号化，存储在机器中，又为它编制了程序。这种程序能模拟人的推理方式，当你把定理的前提和结论以某种规定的符号形式输入到机器中以后，程序不断地尝试在公理、规则和前提中进行查找和推导，直至获得与结论相同的结果。计算机证明定理能力的大小，主要取决于证明程序的好坏和所存储的公理与规则的多少。程序设计得越好，存储的公理与规则越多，计算机证明定理的能力越强。当然，存储的公理与规则多了，程序的效率会受到影响。

下面，看一个简单的例子。

考虑图1给出的图形，设计算机已存入了关于图1的公理：

公理1：对任意的由X、Y、U、V四个顶点构成的梯形，其中X是左上顶点，Y为右上顶点，U为右下顶点，V是左下顶点，VY是对角线。如果XYUV是一个梯形，则线段XY平行于线段UV。

公理2：如果XY平行于线段UV，则∠XYV和∠UVY相等。

图1

给定一个如图2所示的梯形ABCD，线段DB是该梯形的对角线，要证明两个内错角∠ABD和∠BDC相等，即要证明：如果ABCD是梯形，则∠ABD和∠BDC相等。

图2

输入到计算机的前提是：由A、B、C、D四个顶点构成一个梯形，其中，A是左上顶点，B为右上顶点，C是右下顶点，D是左下顶点，DB是对角线，ABCD是梯形。结论是：∠ABD和∠BDC相等。

程序根据前提找到公理1，将公理1中的变量X、Y、U、V分别替换为A、B、C、D，获得公理1的一个实例：如果ABCD是一个梯形，则线段AB平行于线段CD。又因“ABCD是一个梯形”是前提，于是得到中间结果，即公理1实例的结论：线段AB平行于线段CD。再由该中间结果找到公理2，将公理2中的变量X、Y、U、V分别替换为A、B、C、D，获得公理2的一个实例：如果AB平行于线段CD，则∠ABD和∠BDC相等。此时，中间结果“线段AB平行于线段CD”，与公理2实例的前提一致，于是得到结果，即公理2实例的结论：∠ABD和∠BDC相等。这正是要得到的结论，所以，定理得证。

我们这里只是非形式地叙述了计算机证明定理的过程，实际上，计算机证明定理完全是符号化和形式化的。

自20世纪50年代，计算机证明定理从设想阶段走向实验阶段，并且获得了许多可喜的成绩。1956年，纽厄尔等人将人脑演绎推理的思维过程、规则、策略、技巧、简化步骤等编进计算机程序，证明了罗素-怀特海《数学原理》第二章52条定理中的38条。1963年，经过改进的程序证明了全部52条定理。1958年，美籍华人王浩编写的三个程序比纽厄尔等人的程序还简单有效，5分钟就证完了这52条定理。1965年，鲁滨逊提出了归结原理，以其形式的简明而易于机械地实现促进了在计算机上实现定理证明的发展。

我国科学工作者在计算机证明定理的研究上取得了令人瞩目的进展，受到国际学术界的重视和高度评价。其中，吴文俊教授的研究成果最为显著。在1976年和1977年之间，吴文俊找到了几何定理的机械化证明方法，并在计算机上证明了100多条定理。后来，他又把机器证明的范围推广到仿射几何、圆几何、球几何和非欧几何等领域。

由此看来，人可以使计算机具有证明能力。研究计算机证明定理的目的是让计算机直接介人人的思维活动过程，代替人的部分脑力劳动，提高人类科学创造的能力和效率，意义重大而深远。这方面，还有很多的研究工作要做。

关键词：逻辑推理 定理证明 机器证明