简述：机器证明是使用计算机证明定理，也称为定理的机械证明或自动证明。作为计算机科学的一个重要课题，它的研究与发展至今约有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) α→(β→α) (A1)
(2) (α→(β→α))→((α→β)→(α→α)) (A2)
(3) (α→β)→(α→α) (M)(1)(2)
事实上，我们的思路可以是这样的：由待证明的 (α→β)→(α→α)，对照看三类公理的特点，您不觉得眼前一亮：公式(α→β)→(α→α)可对应于(A2)的右端，让α代替r；毫无疑问由规则(M)，我们希望α→(β→α)成立，而这是(A1)！我们就可以写下这个证明序列了。
对于复杂的问题，这“眼前一亮”，对人类来讲也绝非一个轻松的工作。更何况，我们希望我们的计算机也可以“眼前一亮”！
机器证明是困难的，但仍不是没有希望做的完美些。希望您不至于对理论科学感到厌烦。下次我们将展开机器证明的奥秘。
注1：好的数理逻辑教材，我所读的，有
[陆钟万]. 面向计算机科学的数理逻辑. 科学出版社，1998
[王捍贫]. 数理逻辑. 北京大学出版社，1997
本文参考资料：
[陆钟万]. 数理逻辑与机器证明. 科学出版社，1983
[王捍贫]. 数理逻辑. 北京大学出版社，1997
