自动定理证明（Automatic Theorem Proving）是指利用计算机证明非数值性的结果，即确定它们的真假值。

图1-28　早期的自动定理证明机　

在数学领域中对臆测的定理寻求一个证明，一直被认为是一项需要智能才能完成的任务。定理证明时，不仅需要有根据假设进行演绎的能力，而且需要有某种直觉和技巧。

早期研究数值系统的机器是1926年由美国加州大学伯克利分校制作的（见图1-28）。这架机器由锯木架、自行车链条和其他材料构成，是一台专用的计算机。它可用来快速解决某些数论问题。素性检验，即分辨一个数是素数还是合数，是这些数论问题中最重要的问题之一。一个问题的数值解所应满足的条件可通过在自行车链条的链节内插入螺栓来指定。

自动定理证明的方法主要有四类：

1）自然演绎法

它的基本思想是依据推理规则，从前提和公理中可以推出许多定理，如果待证的定理恰在其中，则定理得证。(www.daowen.com)

2）判定法

它对一类问题找出统一的计算机上可实现的算法解。在这方面一个著名的成果是我国数学家吴文俊教授于1977年提出的初等几何定理证明方法。

3）定理证明器

它研究一切可判定问题的证明方法。

4）计算机辅助证明

它以计算机为辅助工具，利用机器的高速度和大容量，帮助人完成手工证明中难以完成的大量计算、推理和穷举。

1976年，美国伊利诺斯大学哈肯和阿佩尔，在两台不同的计算机上，用了1 200小时，进行了100亿次判断，终于完成了四色定理的证明，解决了这个存在了100多年的难题，轰动了世界。