70年代后期，在计算机技术大发展的背景下，吴文俊继承和发展了中国古代数学的传统（即算法化思想），转而研究几何定理的机器证明，彻底改变了这个领域的面貌，是国际自动推理界先驱性的工作，被称为“吴方法”，产生了巨大影响。吴的研究取得了一系列国际领先成果并已应用于国际上当前流行的符号计算软件方面。

人物简介

机器证明介绍：(简述 关键字 举例 数理逻辑的主要特点 试探法)

人物简介

吴文俊，男，1919年5月出生于上海，1940年毕业于上海交通大学数学系。1979年至现在任中国科学院系统科学研究所副所长、名誉所长、研究员。

吴文俊院士是著名的数学家，他的研究工作涉及到数学的诸多领域。在多年的研究中取得了丰硕成果。其主要成就表现在拓扑学和数学机械化两个领域。他为拓扑学做了奠基性的工作。他的示性类和示嵌类研究被国际数学界称为“吴公式”，“吴示性类”，“吴示嵌类”，至今仍被国际同行广泛引用，影响深远，享誉世界。

用计算机自动证明某一类型几何定理，甚至某一种几何全部定理的原理和方法。从理论角度看，几何定理的机器证明要经历公理化、代数化与坐标化、机械化等步骤，才能编制程序并在计算机上实现。可用机器证明的几何定理（主要是初等几何的定理）有三种不同类型，与之对应则有三种不同的机器证明方法。每一类型定理的机器证明都必须假设代数化与坐标化已经完成，而且可把几何定理的证明问题化为一些代数关系式的处理问题。①第一类型定理的特征是假设部分的所有代数关系式对于某些特定变量都必须是线性的，包括一类构造型的纯交点定理，其对应的机器证明方法称为希尔伯特方法；②第二类型定理的特征是假设和终结部分的代数关系式都可用多项式的方程来表示，其对应的机器证明方法是中国数学家吴文俊首先提出的,称为吴文俊方法;③第三类型定理的特征是假设和终结部分可以是任意的多项式等式或不等式，但其系数必须在一实闭域中，因而原来的几何必须有次序关系，其对应的机器证明方法称为塔斯基方法。这三种方法各有其适用范围，但就可以通用的那些定理证明问题来说，希尔伯特法效率最高而塔斯基法效率最低，但是前者的适用范围很窄。1980年在 HP9835A机上，用吴文俊方法成功地证明了勾股定理、西姆逊线定理、帕普斯定理、帕斯卡定理、费尔巴哈定理,并在45个帕斯卡点中发现了20条帕斯卡圆锥曲线,这种方法还推广到微分几何，将微分几何曲线论中的贝屈朗定理推广到仿射微分几何。吴文俊的研究成果引起了国际学术界的重视。

参考书目

吴文俊著：《几何定理机器证明的基本原理（初等几何部分）》，科学出版社，北京，1984。

机器证明介绍：

简述

：机器证明是使用计算机证明定理，也称为定理的机械证明或自动证明。作为计算机科学的一个重要课题，它的研究与发展至今约有50年的历史。在本文中，将试图向您展示机器证明的基本思路和方法。

关键字

： 机器证明，演绎推理形式系统p，试探法，判定法，计算机辅助证明，证明算法

各门的科学中，都有推理和论证；尤其是在数学中，要通过推理和证明来建立定理，证明的每一个步骤都是通过逻辑推理的规则推出另一些命题。从它们出发进行推理的命题称为前提，由此而推出的命题称为结论。

举例

我们来看一个例子。数学分析研究函数的连续性的时候，证明了由下面的前提

1) 函数f(x)在闭区间[a,b]上连续，

2) f(a)与f(b)异号。

能推出结论

3) 有c，使得a<c<b,f(c)=0

但如果把1)中的闭区间[a,b]改为开区间(a,b)，那么由改变后的1)和2)前提就不能推出3)这个结论。

这项工作（推理与证明），一直是由数学家来做的；这是他们的生计。但是，是否有其他的可能？比如，将可用机器来证明和推理数学定理？这是件有意义而又艰难的工作；推理和证明是智能的体现，而人工智能，是人类一直的梦想之一。这需要几个条件。

首先，我们要把推理和证明作为研究对象，加以详细研究。以往的任何数学分支，都有自己的研究对象，但都不研究它们所共同使用的逻辑推理规则；数理逻辑则是这样的一个条件，它把推理和证明作为数学对象来研究。只有对推理和证明等人类思维活动本身有足够的认识，我们才可能把这项工作交给机器来做。

其次，计算机必须有相当的发展。这是毫无疑问的，但往往是相互促进，而并非一方完美后，另一方才能发展。

有了这些条件后，如果产生了需要，机器证明将成为可能；而事实上这种需要产生了。

下面我们将试图展示机器证明的奥秘。可是，本文非正规的学术论文，所以您将看到并不严格的描述和形式化工具交替出现的情况。但介绍机器证明，是本文毫无疑问的目的。

当然，需要简单引述数理逻辑的知识。数理逻辑以推理和证明作为数学对象来研究，它起始于莱布尼茨试图对思维符号化的工作。到如今以是硕果累累，有着丰富的知识体系。一般本科阶段可接触到命题逻辑和谓词逻辑部分，而研究生阶段将详细研究其它高等数理逻辑内容（计算机专业的教学计划）。我们以最简单的命题逻辑“演绎推理形式系统p”为例让您初步了解数理逻辑的特点。

数理逻辑的主要特点

是“形式化”，具体的讲，就是把“数学推理”形式化。而通俗一点，则是把前提和结论，以及前提得到结论这个推理过程都“符号化”为一个系统，形式系统。形式系统具有严格的定义，而这里，您可以暂时认为，形式系统是由4个集合构成：字母表或符号库，字集或公式集，公理集，规则集；公理集是公式集的子集，规则集则是有公式集上的运算构成。

如演绎推理形式系统p的定义：

p的字母表中含有：

(1)命题变元：p1，p2，...，pn，...；

(2)联结词：┐，→；

(3)辅助符号：(，)；

p的公式如下归结定义：

(1)命题变元是公式；

(2)若α是公式，则(┐α)是公式；

(3)若α，β是公式，则(α→β)是公式；

(4)所有公式都是有限次使用(1)-(3)得到。

p的公理集有三类：

(1) α→(β→α) (A1)

(2) (α→(β→r)) →((α→β)→(α→r)) (A2)

(3) ((┐β)→(┐α)) →(α→β) (A3)

p的形式规则:

分离规则：α→β,α┣β (M)

这个系统将胜任命题逻辑的推理证明工作。但是，我给您强调这样一个观念，形式系统中的公式，只是满足一定要求的符号串，在给于它们语义之前，“形式推理”是一列符号串变换。

比如，对于规则(M)：

α→β,α┣β

您不要在心里念叨：如果α为真，α→β为真，则β为真！这是符号串的变换规则，不存在真与假的概念。您不妨就这样看，比如由字符串(公式：)α，可以推出β→α：

(1) α→(β→α) (A1)

(2) α

(3) β→α (M)(1)(2)

这样的一个序列，也就是形式推理。

当然，作为技术人员，我想不看到它的语义部分，大家多半会不放心，这个形式系统p，它有什么用途？但若展开了说，本文就成了数理逻辑的介绍了。这样，有兴趣的读者可参考注1提供的参考资料。

我们来看一看人类的推理证明过程的例子：

在演绎推理形式系统p中证明： ┣ (α→β)→(α→α)

这是个有趣的逻辑思维锻炼，由p的公理集和规则集来推导出这个公式；我想，您可以想到这个序列：

(1) α→(β→α) &n

bsp; (A1)

(2) (α→(β→α))→((α→β)→(α→α)) (A2)

(3) (α→β)→(α→α) (M)(1)(2)

事实上，我们的思路可以是这样的：由待证明的 (α→β)→(α→α)，对照看三类公理的特点，您不觉得眼前一亮：公式(α→β)→(α→α)可对应于(A2)的右端，让α代替r；毫无疑问由规则(M)，我们希望α→(β→α)成立，而这是(A1)！我们就可以写下这个证明序列了。

对于复杂的问题，这“眼前一亮”，对人类来讲也绝非一个轻松的工作。更何况，我们希望我们的计算机也可以“眼前一亮”！

机器证明是困难的，但仍不是没有希望做的完美些。希望您不至于对理论科学感到厌烦。下次我们将展开机器证明的奥秘。

注1：好的数理逻辑教材，我所读的，有

[陆钟万]. 面向计算机科学的数理逻辑. 科学出版社，1998

[王捍贫]. 数理逻辑. 北京大学出版社，1997

本文参考资料

：

[陆钟万]. 数理逻辑与机器证明. 科学出版社，1983

[王捍贫]. 数理逻辑. 北京大学出版社，1997

机器证明，一个出发点，就是“寓理于算”，但这条路并不平坦。数理逻辑大家在探讨思维的符号化工作，计算机科学家也在探索计算机本身的能力极限。一代一代的人，在思索，人类的智慧的奥秘何在；机器如何完成这项工作，如何做的更好，乃至和人类一样好？

上次说到这个公式的证明：

┣ (α→β)→(α→α)

它的证明序列很简单，如下：

(1) α→(β→α) (A1)

(2) (α→(β→α))→((α→β)→(α→α)) (A2)

(3) (α→β)→(α→α) (M)(1)(2)

我在介绍证明思路形成的过程时，曾用到词语“眼前一亮”，但之于科学，这个描述是不好的。在这个问题上，张景中先生曾论述过关于几何定理证明中的人类证明与机器证明过程的异同，我加以扩充，描述如下：

(1)检验：对所有已知条件进行观察和计算，以确定命题；

(2)搜索：依据已有的（常用的）引理和结论，寻找更多的可知信息，如果这些结果不能达到目的，就把它 们作为进一步工作的基础；

(3)规约：从结论出发，利用已知信息消去所依赖的某些已知量和条件，使结论的真假趋于明显或易于检验；

(4)转化：改变命题的形式；如考虑传递律和反证法。

手段(1)的机器模拟已经实现。手段(3)的研究取得了最大的成功，吴文俊先生的几何定理证明方法，就属于此类。(2)则是比较传统的常规手段，是规约的补充和转化基础。而手段(4)，充分体现了人类思维的灵活性和丰富性，目前还难于机械化。

上例子的思路形成，可以体现这些结论。然而毫无疑问，即使手段(4)的完美机械化，也需要我们的进一步努力；更何况，我想机器证明，待开拓的地方还远不止这些。

那么，让我们开始沿着历史的脚步，来细致的看一下，机器证明中的试探法，计算机辅助证明，判定法和证明算法等研究方向的思路；希望我们都能于此感到美妙的兴趣，并有所乐。乐之乃我的目的，不过您若准备自己动手查资料，想深入下去，我则手舞足蹈了。

试探法

使用试探法证明定理，可以从前提出发，或者从结论出发。

从前提出发，就是由前提（包括公理、定义、已证明的定理以及所要证明的定理的假设）中的某些命题推出若干命题作为中间结论；再把中间结论加到前提之中，又推出若干中间结论。如此下去，若推出了所要的结论，则定理得到证明，否则就要考虑其它的途径，从前提的另一些命题推出另外的中间结论，试探推出待证明定理。

从结论出发，则是考虑有了怎样的命题就能推出所要的结论，从而归约为证明这些命题；类似于上面的过程，若定理的前提包括了所需要的命题，则定理得到证明，否则仍需考虑另外的途径。

试探法是一种手段，使用它只是有可能得到问题的解，但并不保证一定能得到解。而且，在定理得到证明之前，我们不能肯定它是不是不可证明的。

在历史上，Newell-Shaw-Simon曾用试探法证明命题逻辑中的重言式。他们使用的形式系统，不是自然推理系统，而是重言式系统，即我们上次介绍的命题推理形式系统p。下面是他们的试探法：

设要证明的A是形式定理，把A看作所要解决的问题。

第一步，试验代入规则。比如：由α→(β→α) 可以推出：

α→((α→β)→α)，

(α→β)→(β→(α→β))，

如果能用代入规则由存储在“形式定理表”中的某个形式定理（包括形式公理）推出A，证明结束；否则代入规则无效，转入下一步。

第二步，试验分离规则。在形式定理表中寻找(B→A)形式的公式，若有，则问题就由证明A归约为证明B，B称为子问题。于是使用B试验代入规则给以证明：如果B能够得到证明，则A的证明结束，否则把B送入“子问题表”。于是继续试验分离规则，若找不到(B→A)形式的公式，转入下一步。

第三步，试验蕴涵词传递规则。蕴涵词传递规则不是定义中的一部分，它可由定义证明，但它非常有用，具体如下：

α→β，β→r┣α→r (Tr)

具体方法为，先检查A是不是蕴涵式，如果不是，则不能进行第三步，于是在子问题表中取出下一个公式，转第二步；如果A是蕴涵式，例如有B→D形式的公式，则在形式定理表中找B→C或C→D形式的公式，若找到B→C形式的公式，则问题由证明A（即B→D）归约为证明C→D，而若找到C→D形式的公式，则问题归约为证明B→C。B→C或C→D是子问题，于是对之进行代入规则证明。若这个证明成功，则证明结束，否则把子问题存入子问题表，继续在形式定理表中寻找B→C或C→D形式的公式，并且重复方才的过程，如果找不到，则在子问题表中取出下一个公式，并转入第二步。

以上证明A的过程中，停机条件是下面四种情形之一：A得到证明；机器时间用完；机器存储器用完；子问题表中的公式用完。因此，当证明过程结束时，A并不一定能得到证明。

著名数理逻辑学家王浩曾给出一个算法，比这个试探法要简捷的多，证明了罗素的巨著《数学原理》中的几百条关于命题逻辑的定理，仅用了9分钟。这是一项意义深远的工作。有兴趣深入的读者可查阅注释2提供的参考资料。

今天我们的旅程暂且到此，下次我们接着今天的足迹。热切的感谢您对理论科学的关注。

注2：[王浩]. Toward Mechanical Mathematics , IBM Journal for Research and Development ,4,224-268,1960

本文参考资料：

1，[陆钟万]. 数理逻辑与机器证明. 科学出版社，1983

2，[张景中]. 几何定理机器证明研究展望. 中国科学院院刊第二期，1997