第 2 章　自动定理证明兴衰纪

As a material machine economises the exertion of force, so a symbolic calculus economises the exertion of intelligence...the more perfect the calculus, the smaller the intelligence compared to the results.

就像机器能省体力一样，符号演算能省脑力。

演算越完美，付出的脑力就越少。

——W. E. Johnson（约翰逊）

　

Proof is cultivated reasoning.

证明就是讲究的推理。

——Bruno Buchberger（布赫伯格）

数学哲学有三大派：逻辑主义、形式主义和直觉主义。逻辑主义的代表人物是罗素，主旨是把数学归约到逻辑，这样只要把逻辑问题解决了，之上的数学问题自然就解决了。也就是说，把逻辑玩转了，数学就不算事儿。希尔伯特主导的形式主义是另一派，他的梦想是把数学形式化，数学过程就是把一串符号变成另一串符号。希尔伯特设想，如果能设计一个大一统的算法，那么所有的数学问题都可以由这个算法来解答。这和逻辑主义精神有一定相通之处。哥德尔后来证明这一切是不可能的。机器定理证明的研究从某种意义上继承了罗素和希尔伯特的思想：用机器来证明和判定那些可以证明和判定的问题。纽厄尔和司马贺的“逻辑理论家”就是早期的机器定理证明程序，他们曾经给罗素写信，期盼能得到伟人的首肯，罗素在回信时说：“我相信演绎逻辑里的所有事，机器都能干。”

自动定理证明起源于逻辑，初衷就是把逻辑演算自动化。逻辑学的源头是亚里士多德的三段论。现代逻辑的奠基人是弗里格（Gottlob Frege）和罗素。弗里格用函数表示谓词，英国人约翰逊（W. E. Johnson）和意大利人皮亚诺使用(x)表示全称，∃x表示存在。这样，“人总有一死”，在一阶逻辑中就可表示为(x)Mortal(x)，翻译成普通话就是：“对所有的人x，x必有一死。”1935年德国人根岑（Gerhard Gentzen）仿照∃[exist（存在）的首字母E的反写]引入符号∀[all（所有）的首字母的反写]更鲜明地表示全称。根岑的老师是犹太人伯奈斯（Paul Bernays），希尔伯特的合作者。伯奈斯被纳粹赶出德国后，根岑接替老师做了希尔伯特的逻辑助手。根岑是纳粹冲锋队的早期成员，战时积极参与德国导弹V-2的研发，1945年饿死在布拉格的战俘营。他是数理逻辑四大分支之一证明论1的奠基者之一，证明论和自动定理证明有着密切的关系。

1数理逻辑四大论是模型论、证明论、递归论（即可计算理论）和集合论。

人工智能中符号派的思想源头和理论基础就是定理证明，不懂定理证明就没法深入了解符号派。尽管纽厄尔和司马贺的“逻辑理论家”在人工智能圈子开风气之先，但它还真不是第一个可运行的定理证明程序。这项“第一”的荣誉应归逻辑学家戴维斯（Martin Davis），他1954年完成了第一个定理证明程序，所用的机器是普林斯顿高等研究院的一台以冯诺伊曼昵称“强尼”（Johnnie）命名的电子管计算机“大强尼”（JOHNNIAC），而文章则迟至1957年才公开发表。

戴维斯是富有成就的数学家和逻辑学家，他比明斯基小一岁，也是著名的纽约布朗克斯科学高中的学生，那学校已经出了7个诺贝尔物理学奖得主，一个化学奖得主。戴维斯家境不好，大学时上了被称为“穷人哈佛”的纽约市立学院（CCNY）——那学校不收学费。在那儿他遇见了坡斯特（Emil Post），是坡斯特指引他走上了逻辑之路。他去了普林斯顿大学读博士，导师是丘奇，但戴维斯对启蒙老师坡斯特的感情远胜于丘奇。他出名后，在各种场合为终生不得志的坡斯特鸣不平，他指出坡斯特在1922年就获得了和哥德尔1931年不完全性定理类似的结果。戴维斯1957年写的教科书《可计算性和不可解性》最早系统地介绍了坡斯特的工作，外界才开始得知坡斯特的名字。戴维斯22岁博士毕业时，23岁的明斯基才刚从哈佛大学本科毕业，正在来普林斯顿大学读博的路上。戴维斯最重要的贡献是和哲学家普特南（Hilary Putnam）等人解决了希尔伯特第十问题。机器定理证明是他一直感兴趣的副业。

戴维斯（1928—　）

戴维斯的定理证明器实现了普利斯博格算术（Presburger Arithmetic）的判定过程。自然数的一阶理论也称皮亚诺算术，包括自然数的加法和乘法，普利斯博格算术是皮亚诺算术的一个子集，它只有加法没有乘法。皮亚诺算术不可判定，但普利斯博格算术则是可判定的。虽可判定，但其计算复杂性是超指数时间的。这样的算法在“大强尼”上是跑不出什么有意思的结果的，但戴维斯还是为证明器跑出的结果激动不已：两个偶数之和还是偶数——如果没有乘法和除法，偶数定义会稍啰唆。值得指出的是，普利斯博格是伟大逻辑学家塔尔斯基（Alfred Tarski）在华沙大学时的学生，他在1928年证明了一阶自然数加法可判定，之后得了个硕士学位就离开学术界，入了保险行。塔尔斯基门下的另一个著名的数学家学生费弗曼（Solomon Feferman）曾说，如果知道普利斯博格工作后来的重要性，真该给他发个博士学位。

后来，戴维斯和普特南继续合作机器定理证明的工作。普特南是20世纪最有影响力的美国哲学家之一，他提出的“缸中脑”（brain in a vat）是最常被引用的假想实验之一，他和戴维斯等人合作解决希尔伯特第十问题，由此又跨入了数学家行列。他是美国共产党分裂后的组织进步劳工党的活跃党员，晚年对政治失望，68岁时行了犹太人的成人礼。戴维斯和普特南合作的成果就是影响广泛的戴维斯-普特南（Davis-Putnam，简称DP）过程，以及后来的DPLL。

普特南（1926—2016）

戴维斯2008年接受美国数学学会杂志Notices of AMS采访时，只讲了希尔伯特第十问题，以及对连续统问题的看法，压根没提他们的机器定理证明工作。与他们的其他工作相比，定理证明真不算什么。在访谈中，他倒是对哥德尔的哲学观点做了点评。他曾在布朗大学听过哥德尔给数学家讲哲学，哥德尔认为大脑和图灵机不等价。而戴维斯相当直率，他认为大脑就是机器，后来为此还和《皇帝新脑》的作者彭罗斯（Roger Penrose）掐过。20世纪80年代末，戴维斯在南开数学所演讲，仗着年轻不知天高地厚，我曾问他怎么看当时风风火火的第五代计算机，因为五代机的核心Prolog毕竟是定理证明的产物，老头狡猾地呵呵说“我对工业不太懂”，他说的工业泛指人工智能。

纽厄尔和司马贺的“逻辑理论家”被认为是AI历史上最重要的原创工作之一，他们的程序可以证明怀特海和罗素《数学原理》第一卷中命题逻辑部分的一个很大的子集。但有一段有意思的插曲，他们把文章满怀期待地投给逻辑学最重要的刊物《符号逻辑杂志》（Journal of Symbolic Logic，JSL），却惨遭主编克里尼（Stephen Kleene，丘奇的另一位学生）退稿，理由竟然是：把一本过时的逻辑书里的定理用机器重证一遍没啥意思。其实克里尼并非反对机械化的工作，1955年《符号逻辑杂志》就发表过逻辑学家蒯因（W. V. Quine，王浩的老师）的一阶逻辑证明过程的文章，这种理论杂志关注的是有没有原创性，能不能实现倒不是那么重要。蒯因的这篇文章成为后来一批工作的基础。

“逻辑理论家”中首创的“启发式”程序对人工智能和心理学有意义，但逻辑学家却不买账，以至于一些早期的定理证明文章的题目中竟然出现“非启发式程序”的字样，故意恶心纽厄尔和司马贺。王浩甚至称“逻辑理论家”是一个“不专业”的工作，并说“杀鸡焉用宰牛刀，但他们（指纽厄尔和司马贺）拿着宰牛刀也没能把鸡杀了”。这些批评导致做自动定理证明的数学家和逻辑学家在很长一段时间都谨慎地和人工智能圈子保持着若即若离的关系，很多人宁可和计算机理论家混在一起，也不掺和人工智能。

“逻辑理论家”之后，在理论和实践都很有影响的工作是普拉维茨（Dag Prawitz）的自然演绎（natural deduction），自然演绎可以追溯到根岑。普拉格维茨设计了一个程序语言实现了他的算法，那时不要说编译，连汇编语言都没有。普拉格维茨的老爸在1957年夏天把儿子的程序手工编译成一台瑞典制造的计算机的机器代码。那台机器有2K 40位内存（相当于10K字节）和40K字节的磁鼓外存。于是老普拉格维茨也成了那篇影响深远的文章的作者之一。这项工作不只是自然演绎的开篇，还提出了合一（unification）的概念。

明斯基晚年自诩地回忆自己在达特茅斯会议期间，当场在纸上画了一个几何定理证明器的设计草案，并手动模拟证明了等腰三角形的一个定理。这不禁让我们联想到当下在草纸上当场写商业计划书并得到巨额风险投资的神话，这一类段子的“始作俑者”是明斯基，虽不知这事能否全信，倒也符合明斯基的个性。达特茅斯会议后的1956年9月，IBM招了新毕业的物理学博士格兰特（Herb Gelernter）来实现明斯基的几何定理证明器，1957年觉得人手不够，又从宾夕法尼亚州立大学招来了逻辑学家吉尔莫（Paul Gilmore）帮忙。为了学习IBM 704上的汇编语言，吉尔莫决定先试着实现语义表（Semantic Tableau）方法，最后的结果居然和普拉格维茨异曲同工，但他在一年后才得知普拉格维茨的工作比他要早一年。

1958年夏天，王浩也在一台IBM 704机上实现了一个完全的命题逻辑程序，以及一个一阶逻辑程序。后者只用9分钟就证明了《数学原理》中一阶逻辑的全部150条定理中的120条。到1959年夏天，改进版本证明了全部150条一阶逻辑以及200条命题逻辑定理。例如，《数学原理》中的定理*11.26被罗素和怀特海写为：

*11.26. |--:.(∃x):(y).Φ(x,y):⊃:(y):(∃x).Φ(x,y)

现代教科书的记法是：

(∃x)(∀y)Φ(x,y)⊃(∀y)(∃x)Φ(x,y)

如果Φ(x,y)表示“x和y是一双鞋”，这句话可以翻译为“如果存在一个x对所有的y都能配成一双鞋的话，那么对所有的y，都必定存在一个x能和它配成一双鞋”。不知道x和y哪一只是水晶鞋。

王浩在打孔卡片上的记法则是：

11*26/EXAYGXY-AYEXGXY

很明显这是为了节省复杂公式的语法解析（parsing）成本，这里E就是存在量词∃，A就是全称量词∀。

当然《数学原理》中罗列的一阶逻辑定理只是一阶逻辑的一个子集。王浩注意到《数学原理》里的一阶逻辑公式都是AE形式（即前面是全称量词，后面是存在量词），后来他又继续研究AEA的可计算性和复杂性，由此引出了他的学生库克（Stephen Arthur Cook）的NP理论——库克1971年发表的文章的题目恰好是《定理证明的复杂性》，因此获得1982年图灵奖，可以公正地说，王浩的定理证明研究孕育了整个理论计算机科学。库克在回忆老师时说：“我很了解王浩的思想和方法，我对NP完全问题的结论与他非常相似。图灵和王浩研究谓词逻辑，我研究命题逻辑。”

王浩以哥德尔的权威诠释者和知音名世，但他对哲学、逻辑学、计算机科学的原创贡献却被低估了。王浩一共只培养过5个学生，都是20世纪60年代他在哈佛大学教数学和逻辑时，之后他离开逻辑学和计算机科学，专心于哲学了。与此对照，他的学生库克则有34个学生，库克至今仍活跃在本领域的前沿。

哥德尔（1906—1978）与王浩（1921—1995）

1983年，国际人工智能联合会（IJCAI）授予王浩自动定理证明里程碑大奖，王浩在致获奖词时半开玩笑地说因为自己的个性，荣誉经常绕道而行。这和他老师蒯因对他的印象截然不同，蒯因认为王浩一直不满现状，并不断跳槽。王浩回忆起若干年前，他在洛克菲勒大学的顶头上司李德伯格（Joshua Lederberg）校长给他推荐了雷纳特（Douglas Lenat）的博士论文。那是关于用机器进行启发式数学学习的，一段时间内在人工智能界很有影响。但王浩看后觉得雷纳特的东西基础不牢靠，逻辑学家自然有资格随时对计算机科学家说三道四。作为诺贝尔生理学或医学奖获得者，李德伯格在成为洛克菲勒大学校长之前是斯坦福大学的遗传系主任，一直在和雷纳特的老师费根鲍姆合作，用人工智能技术解决化学问题，他们合作的成果就是第一个专家系统Dendral。其实，雷纳特也意识到自己早期工作的问题，他后来走上了一条30年的不归路——Cyc，用逻辑表达人类的常识，为现今的知识图谱奠定基础、积累经验。这是后话。

王浩的定理证明程序后来成为高级语言的基准程序，麦卡锡的LISP早期就一直以王浩算法的程序作为例子。王浩对“逻辑理论家”的批评后来被哲学家德雷弗斯用来攻击AI，这也使王浩不爽。尽管王浩的工作被人工智能学界渐忘，但他的逻辑圈朋友都十分认可。

戴维斯的几篇关于定理证明历史的文章题目下面都不忘写一行“纪念王浩”。王浩毕业于神奇的西南联大数学系，曾和杨振宁同屋，“二战”结束后又到清华大学在金岳霖和王宪钧指导下得了哲学硕士，到哈佛大学后跟随美国最有影响力的哲学家蒯因研究逻辑和分析哲学。20世纪50年代，王浩曾一度想回国效力，于是他从哲学转向计算机，因为计算机更加实用，对祖国建设的贡献更加直接。戴维斯证实，王浩在收到他父亲指责他的信之后放弃了回国的念头，他认为他父亲的信是在压力之下写的。关于这段历史见尼克《哲学评书》。王浩没能回国，而机器定理证明则成为王浩计算机科学转向期间的一个插曲。

1957年夏季，在塔尔斯基的号召下，一个逻辑学家的大聚会在康奈尔大学举行，会上数学家亚伯拉罕·罗宾逊2（Abraham Robinson）指出，埃尔布朗（Herbrand）定理可以把一阶逻辑的问题转化为命题逻辑。这激发了大家寻求统一高效的定理证明的实现方法。

2数学和逻辑领域有好几个罗宾逊，且互有关联。

英国人阿兰·罗宾逊（John Alan Robinson）1952年在剑桥得了古典学学位后来到美国，1956年在普林斯顿大学哲学系亨培尔（Carl Hempel）指导下得了博士，但他的实际导师是年轻的普特南。有意思的是，罗宾逊在读博士时并不知道导师普特南正在和戴维斯合作研究机器定理证明。罗宾逊毕业后先是到杜邦公司研究运筹学，1961年他谋得在赖斯大学（Rice）哲学系教逻辑的职位，但每年夏天还是到阿贡国家实验室做机器定理证明的研究。后来他索性全职加入了刚成立的阿贡定理证明小组，一位同事是和他同姓的软件工程师乔治·罗宾逊，另一位就是随后成为阿贡定理证明小组的头儿的传奇人物、盲人数学家沃思（Larry Wos）。事实上，是哲学家罗宾逊和“码农”罗宾逊用蒯因的入门教科书《逻辑方法》教会了数学家沃思逻辑。阿兰·罗宾逊一开始的任务是实现DP（戴维斯-普特南）过程，这回还是用IBM 704，但此时已经有了高级语言Fortran。在实现DP的过程中，他发现了对后来定理证明有长远且深刻影响的归结（resolution）原理。有时，一个重大的发现或发明是在深刻体会已有工作的过程中自然出现的。相关文章的发表却因为一名匿名审稿人的疏忽而耽搁，迟至1965年才公开发表在JACM上。

阿兰·罗宾逊（1930—2016）

阿兰·罗宾逊受到普拉格维茨工作的启发，拓展了普拉格维茨的原始合一算法，发明了归结原理。以前的定理证明技术会用到很多规则，有了归结后，所有的证明推导只要有归结这一条规则就可以了。据后来考证，归结方法在1937年就被布莱克（Archie Blake）在其关于布尔代数的博士论文中发现过，而蒯因在1955年简化布尔函数时也独立发明过。但无论如何，把合一算法和归结原理结合并应用到一阶逻辑是罗宾逊的原创，这是定理证明中的重要里程碑。

在罗宾逊1965年的文章中，一个被忽视的贡献就是包含（subsumption）。虽然归结极大地简化了定理证明，但是它的一个副作用是可以很快生成大量新子句，这和其他定理证明技术是类似的。大部分新子句是没必要保存的，这就像图书馆时不时要清理旧书，相当一部分书的内容已经被另一部分书所包含。例如我们知道“所有人必死”Mortal(x)，那么当生成“苏格拉底必死”Mortal(Socrates)作为中间子句时，它没必要被存下来，也就是说Mortal(x)包含了Mortal(Socrates)。沃思等人在1991年纪念罗宾逊六十大寿的文集上撰文指出包含是罗宾逊的另一大贡献，其重要性甚至要超过归结原理。罗宾逊的贡献不能单纯用归结来总结，他的原创性在于一系列工作的综合，除了归结外，还有合一和包含。

项重写（term rewriting）其实就是数学哲学中希尔伯特形式主义的精髓：证明就是将一串公式重写成另一串公式。例如，乘法的分配律就是：

a(b+c) →ab+ac

“→”左边的公式被重写成右边的公式。重写规则就是单向的方程。方程式（等式）是一阶逻辑的子集，即只有一个谓词EQUAL。仿照哥德尔的一阶逻辑完全性证明，美国数学家伯克霍夫（George David Birkhoff）证明了方程逻辑是完全的。考虑到方程在数学中的广泛使用，方程逻辑一直是逻辑中一个活跃的领域。数学活动都可以被看作对公式的重写，方程式求解的机械化的重大突破是算法大师高德纳（Donald Knuth）和他的学生本迪克斯（Peter Bendix）做出的。他们的工作为项重写提供了坚实的基础，重要性不亚于罗宾逊的归结原理。如果说罗宾逊20世纪60年代奠定了逻辑主义定理证明，高德纳和本迪克斯则在1970年开启了形式主义证明方法。

从某种意义上说，丘奇的λ演算就是项重写。针对谓词是等词的情况，沃思等人则提出了 paramodulation和demodulation（项重写的一种简单变种）。paramodulation后来被推广为superposition，成为现代定理证明器的理论和实践基础。

芝加哥大学的实验物理学家费米在曼哈顿计划的早期负责核反应堆。战后，美国以费米实验室为基础建立了第一个美国国家实验室阿贡（Argonne），隶属于美国能源部。阿贡国家实验室的一个分部是应用数学和科学计算，阿贡定理证明小组就在这个分部。阿贡小组对机器定理证明的贡献是决定性的和全方位的。罗宾逊就是在阿贡工作时提出了归结原理。阿贡为归结原理的实现提供了一整套生态环境。小组的头儿沃思尽管是盲人，却是数学天才，他14岁就赢得芝加哥大学的奖学金，但他等到17岁生活能自理后才入学。

计算机科学的大部分分支要求不只是理论好，还得能构建系统。阿贡小组的精神就是实战。小组的另一员干将欧文白克（R. Overback）曾和摩尔（J Strother Moore）讨论理论和实际之争，摩尔说：“编程就像做爱，没法叫别人替你干。”阿贡小组除了paramodulation，还提出了支持集（Set of Support，简称SoS）的概念。在证明定理中，通常会把给定的公理和待证的结论分开，一般不会在公理内互相归结，这样可以极大地提高定理证明的效率。支持集就是公理之外的子句集。其实人在证明定理时也是如此。沃思证明支持集是完备的。

除了技术方面，沃思为定理证明做出的最大贡献就是把马库恩（William McCune）招到阿贡实验室。马库恩遂成为20世纪90年代定理证明领域快速发展的重要推动者。他理论实践两手都硬。在加入阿贡实验室后，他用C语言写了Otter定理证明器，Otter实现了当时定理证明里最先进的所有技术。美国人工智能的主要语言是LISP，马库恩和人开玩笑说他不会写LISP，只会写C。

马库恩（1953—2011）

包含测试是定理证明中最花时间的，很多证明器要花超过95%的时间做包含测试。相比正向包含，反向包含测试有点得不偿失，有些定理证明器选择不做反向测试。马库恩是最早把项索引（term indexing）引入到机器定理证明器的人。Otter主要用到了两种项索引，一种是路径索引（path indexing），另一种是马库恩自己发明的差别树索引（discrimination tree indexing）。差别树索引对正向包含极为有用，正向包含测试是比反向包含测试更耗时的操作，差别树极大地提高了证明的效率。

马库恩还利用Otter的模块开发了另一款专门证明方程的证明器EQP。1996年10月10日，马库恩用EQP证明了罗宾斯猜想。这是数学家罗宾斯（Herbert Robbins）1933年提出的一个关于布尔代数的猜想，60多年来从未被证明。EQP在一台486机上跑了13天给出了证明，之后又在一台IBM RS/6000工作站上跑了7天进行了验证。《纽约时报》马上报道了这一里程碑事件。马库恩在第一时间打电话给已经81岁还在罗格斯大学（Rutgers）任教的罗宾斯，说一开始他们认为罗宾斯猜想的第三公理可能是个印刷错误，罗宾斯听了颇为得意。1957年司马贺曾预言计算机将在10年内击败人类象棋冠军时，还预言10年内机器能证明人没能证明的定理。实际上这花了39年。一年后的1997年，IBM“深蓝”击败了卡斯帕罗夫。

大多数定理证明器都使用反证法，也就是把给定要证明的命题的否命题输入系统，得出矛盾（即空子句），从而证明原命题。定理证明一般只能回答“是”或“否”的问题。有时我们需要证明结果提供更多信息。假设我们面对一个定理证明系统，想知道它是否包含这样的事实“谁是玛丽的丈夫？”那么我们可以问：

～Husband(x, Mary).

也就是问我们想要知道答案的问题的否命题。如果定理证明系统里已经包含了另一条命题：

Husband(John, Mary).

那事情很简单，两个子句归结，产生空子句。我们从而知道“玛丽是有丈夫的”，但我们仍然不知道他是谁。格林（Green）在1969年的斯坦福大学博士论文里想到了一个简单的解决办法——在被要求证明的子句里附加一个系统谓词ANS，那么我们可以问：

～Husband(x, Mary) | ANS(x).

归结后得到ANS（John）。由于ANS是系统谓词，这个结果仍然是空子句。但ANS中包含了我们想要的结果：玛丽的丈夫是约翰。

ANS这个系统谓词已经在Otter这样的定理证明器中得到实现。在Otter中系统谓词都以$开头，$ANS的作用其实就是跟踪变量的值。定理得证时（即子句变空时），$ANS中变量的值就是问题的答案。

纽厄尔在总结AI历史时用了“路线斗争”的方法，即在任何时刻，每种方法都有个对立面。与定理证明密切相关的路线斗争涉及定理证明与问题解决（Theorem Proving vs Problem Solving，1965）以及过程表达与陈述性表达（Procedural vs Declarative Representation，1970-1980）。在这两场争斗的美国主战场，定理证明和陈述性表达的通用性被认为是低效的，没法用来解决实际问题。定理证明的共同体从此分化，分为“纯的”和“不纯的”两派。“不纯的”一派认为必须引入过程表示，而“纯的”一派则认为引入过程知识是“作弊”，智能程序本身也得有智能，只要把问题陈述出来，定理证明程序就应该智能地工作，不必依靠编程者的过程知识。于是，在PLANNER、QA3/QA4等带过程表示的系统和语言被开发出来以后，除了阿贡小组在坚持外，“纯的”定理证明学者在美国的日子并不好过。实际上，把函数恰当地引入ANS谓词中，PLANNER的问题都可转化为一阶逻辑的问题，不多也不少。

纽厄尔总结的另一对对立面就是逻辑与心理（Logic v.s. Psychologic）。他把这段路线斗争的时间区间定在1910年到1945年（1910年怀特海和罗素的《数学原理》出版，1945年麦卡洛克和皮茨的神经网络文章诞生）。这大概与王浩曾不留情面地批评过他和司马贺有关，他们的工作不被逻辑学家认可，当然只能是心理派，而在文中他似乎也认为逻辑与心理之争并没有完结。

符号派的掌权者多是心理派，没受过科班逻辑训练，而理论家又时常会嘲讽逻辑不好的实干家是“民科”。归结原理导致的组合爆炸仍然需要启发式方法的帮助。于是，心理派的人又开始了对逻辑派的攻击，费根鲍姆批评罗宾逊把人工智能引入陷阱。罗宾逊对定理证明的停滞也束手无策，被迫从《人工智能杂志》编委会辞职，最后回归逻辑研究。这也算是费根鲍姆替他老师纽厄尔和司马贺对王浩早年对他们尖刻批评的报复吧。而20世纪80年代初期阿贡小组核心成员温克（Steve Winker）在给一份著名的AI杂志投稿时，资深编辑都懒得把稿件送给匿名评审，只是回信说“也许JACM还在发这类东西吧，尽管我也不知道为啥（他们还发）”。JACM是美国计算机学会会刊，以发理论文章著称。联想到早些时候，纽厄尔和司马贺关于“逻辑理论家”的论文惨遭《符号逻辑杂志》主编克里尼退稿，我们只好感叹“冤冤相报何时了”。欧文白克愤怒地回忆某知名人工智能新秀对归结原理的不屑，那位后来变成权威的人士批评基于归结的定理证明器不能解决实际问题。欧文白克多年后说权威这辈子都没能干出一个可以工作的系统，而马库恩的EQP已经证明了罗宾斯猜想。

归结的简单性引起了人们的重视，但它同样有组合爆炸问题，在人们对如何驾驭归结没有理论和经验的共识之前，整个领域早已改朝换代，问题解决与否，已经无人关心。20世纪70年代后，阿贡小组依然是美国定理证明的堡垒，但整个学科的研究重心逐渐从美国转向欧洲，特别是英国，在那里，逻辑程序应运而生，成为后来日本五代机的理论基础。

哥德尔证明一阶整数（算术）是不可判定的，但几乎在同时塔尔斯基则证明一阶实数（初等几何和代数）是可判定的。塔尔斯基的证明结果直到“二战”后在美国成书才得到更为广泛的流传。塔尔斯基一直自认为他应该是和哥德尔比肩的逻辑学家。冯诺伊曼在得知哥德尔不完全性结果时曾半开玩笑地说，要是哥德尔的结果晚出来几天，他说不定就能证明一阶逻辑是完全的呢。塔尔斯基的结果意味着可以存在算法能对所有初等几何和代数问题给出证明。塔尔斯基的原始算法是超指数的，在被后人多次改进之后仍然很难被当作通用算法。数学家吴文俊在研究中国数学史时，受到启发，针对某一大类的初等几何问题给出了高效的算法。后来吴文俊的方法还被他推广到一类微分几何问题上。

吴文俊（1919—2017）

王浩在得知吴文俊的结果后马上给吴文俊写信，建议他利用已有的代数包，甚至考虑自己动手写个程序实现吴的方法。其实，后来塔尔斯基算法的各种改进都被吸纳进数学程序包Mathematica中了。不严格地说，如果哥德尔系逻辑的机器体现是图灵机的话，塔尔斯基系逻辑的机器体现就是实数模型。王浩和吴文俊的通信大概是哥德尔系定理证明和塔尔斯基系定理证明为数不多的交流。

王浩1978年4月10日写给吴文俊的信

目前，基于逻辑的定理证明器最适合解决代数问题。而几何定理证明器却又都是基于代数的。王浩是逻辑系定理证明的先驱，吴文俊则开几何系定理证明的风气之先。哥德尔定理和塔尔斯基定理在人工智能问题上各有蕴意，是为后话。有意思的是，塔尔斯基对机器定理证明的结果不感兴趣。在1957年康奈尔大学的逻辑学家大会上，他听到戴维斯讲实现他学生普利斯博格的判定过程时如此，甚至在后来听到科林斯和科恩（就是证明了连续统独立性的那位，他非常看不起逻辑，但不曾想当年居然也干过这种脏活累活）改进了他自己的结果时，也无动于衷。这让科林斯很沮丧。

吴文俊是数学家中的人精。“文革”期间，他在北京无线电一厂下放，那是家计算机厂，他开始对计算机感兴趣。他最早和计算机相关的论文是讲怎么利用拓扑学给计算机电路布线的。数学家学会了计算机编程，试试机器证明是最自然的。一开始的算法都是手工推演，1977年大年初一，吴文俊取得了突破。同年，他的文章《初等几何判定问题与机器证明》发表在《中国科学》上。吴文俊声称他的成果是在研究中国数学史时受到的启发。

周咸青（Chou Shang-ching）1978年考到中科院计算所，师从唐稚松，他正好赶上吴文俊开几何定理证明的课，就去旁听了。那时吴文俊的书《几何定理机器证明的基本原理》还没正式出版，但所有旁听生都已拿到手稿。周咸青后来到得克萨斯大学奥斯汀分校留学，师从波尔（Robert S. Boyer）和布莱索（Woody Bledsoe）。他们从周处听说吴文俊的工作很是兴奋，这两位虽都是逻辑系定理证明的大咖，但他们有足够的宽容，让周咸青对自己的博士论文题目自作主张，周的论文基本就是吴方法的实现。奥斯汀分校的硬件设备当然比吴文俊的环境好多了，周取得的成果自然也更加丰富。吴文俊的名字由此传向自动定理证明界。

“文革”后的中科院数学所派系纷杂，乘着华罗庚在欧洲访问，关肇直在中科院副院长钱三强的支持下，迅速成立中科院系统科学所，吴文俊毫不犹豫地跟随关肇直到了系统所。等华罗庚从欧洲回来，生米已然成了熟饭，华罗庚单约吴文俊请他回数学所，被吴婉拒。吴文俊虽和华、关都保持友好关系，但关肇直更理解吴文俊。20世纪50年代，华罗庚曾在数学所建立逻辑组，并邀胡世华领衔。后几经周折，逻辑组先被分派到计算所，后来软件所从计算所分家时，逻辑组再到软件所。直到1998年，原来分出去的几个所才又重新集结在“数学与系统科学研究院”的名下，吴文俊的“数学机械化研究中心”也成了这个新研究院的重要组成部分。研究院的英文名字居然是Academy of Mathematics and System Science，不知道这段历史的，大概会以为他们是和中科院同级的Academy吧。

1979年，吴文俊的工作得到杨振宁的关注，当时的科学院副院长李昌和关肇直都大力支持吴文俊，并为他申请到2.5万美元的外汇到美国购买一台家用电脑，以实现他的吴方法。1979年，普林斯顿高等研究院邀请吴文俊和陈景润访美。吴文俊在普林斯顿讲了拓扑、中国数学史和机器定理证明。普林斯顿的人对机器证明不感兴趣，吴文俊有点失望。吴文俊还顺道访问了加州大学伯克利分校，在那儿见到了菲尔茨奖得主斯梅尔（Steve Smale）。斯梅尔是实数计算模型BSS的原创者之一，他高度评价了吴文俊的工作，这令吴文俊欣慰。斯梅尔出名也是靠拓扑，但晚年转到计算理论，和吴文俊惺惺相惜吧。吴文俊此次访美的重要一站是去王浩所在的洛克菲勒大学。吴文俊的工作在定理证明界迅速引起重视，王浩是另一个关键推手。在波尔和项洁的推荐下，吴文俊1997年获得第四届埃尔布朗奖，这是定理证明领域的最高奖项。

吴文俊的长寿也体现在他的学术生命上。1979年吴文俊60岁高龄开始学习计算机编程语言，先是BASIC，后是Algol，再后是Fortran。他在那台2.5万美元的家用电脑上不断取得新的成果。后来系统所的硬件设施改进，吴文俊相当一段时间都是上机时间最长的。

在定理证明的早期，研究者追求“一招鲜吃遍天”，就是找到一个超级算法能证明所有问题，最典型的例子是归结法和后来的superposition。王浩不认可这种思路，他认为他自己的早期工作和吴文俊的方法都表明最有效的方法是先找对一个相对可控的子领域，然后针对这个子领域的特性，找到有效的算法。

吴文俊后来喜欢用一个比“机器定理证明”更大的词儿“数学机械化”（Mechanization of Mathematics）来描述他的工作，这个说法借自王浩（Wang，1960）。吴文俊的哲学思想是典型的数学家思路，这和逻辑学家不同。数学家把机器定理证明当作工具，而逻辑学家则把机器定理证明当作目标。数学家主要看是否有用，而逻辑学家则看是否纯粹。吴老在一次讲座中讲计算机和数学机械化，引用维纳的说法：“人脑贬值，至少人脑所起的较简单、较具常规性质的判断作用，将贬值。”笛卡儿认为代数使得数学机械化，因而使得思考和计算步骤变得容易，无须花很大脑力。小学算术很难的东西，初中代数立个方程马上就解了。每一次数学的突破，往往以脑力劳动的机械化来体现。

杨振宁曾说他最重要的成就是提高了中国人的自信。陈省身、华罗庚、杨振宁、李政道那一批人都是为人类文明做出突出贡献的中国人。那个不长的名单里还应该有王浩和吴文俊。

迈阿密大学的萨特克里夫（Geoff Sutfliffe）每年都组织机器定理证明大赛CASC（CADE ATP System Competition），主要针对命题逻辑和一阶逻辑证明器。萨特克里夫还维护一个TPTP（Thousands of Problems for Theorem Provers）的网站，这里有大量的定理证明程序的基准测试例题。在2000年之前的大赛中，Otter几乎在所有的领域都力拔头筹。2005年后曼彻斯特大学的“吸血鬼”（Vampire）后来居上，至今一直维持领先状况。

除了命题逻辑和一阶逻辑外，高阶逻辑（主要是类型论）的自动定理证明在欧洲各研究机构一直有人研究。每年“高阶逻辑定理证明”的会议录都被收入斯普林格出版社（Springer）的LNCS系列。

如果说Otter和“吸血鬼”代表了逻辑主义定理证明的高峰，形式主义定理证明器中最广为人知的当属波尔-摩尔证明器及其一系列后续变种。波尔-摩尔证明器的核心是数学归纳法和项重写。波尔-摩尔证明器被用来证明软件和硬件的正确性。有意思的是，他们的另一项工作波尔-摩尔字符串匹配算法（Boyer-Moore string search algorithm）的起因也是定理证明。他们最早用来实现定理证明器的语言是InterLisp，但后来迅速发现InterLisp内带的朴素字符串搜索太慢，他们的算法比朴素算法快了50倍，目前仍是最快的字符串匹配算法，几乎在所有的语言和软件包里都有实现。他们后来又用自己的定理证明器来证明自己的字符串算法的正确性。在2016年5月的维基百科里，Boyer-Moore string search algorithm词条被引用61次，而Boyer-Moore theorem prover（即Nqthm）词条只被引用11次，真是无心插柳啊。

计算机代数的早期研究者都出自明斯基门下，最有名的程序是MACSYMA。Mathematica的作者沃尔弗拉姆（Stephen Wolfram）早期也是MACSYMA的用户。现在Mathematica整合了许多定理证明算法，也有人利用Mathematica作为定理证明的框架和壳子。其实在马库恩用自己的EQP证明了罗宾斯猜想后，就有人用Mathematica来验证。

还有一类定理证明器，其功能主要是作为验证器（proof checker）。荷兰的德布罗金（de Brujin）的AUTOMATH是早期著名的证明验证器。朗道著名的《分析基础》教科书整个被翻译成AUTOMATH的形式语言，形式化证明的长度是原书的10倍。

物理学怪才兼企业家弗雷德金（Edward Fredkin）曾为计算机下棋设立过奖项。但不大为人所知的是，他为机器定理证明也设立过一个奖项，分三等，第三等是当前成果奖（Current），1983年沃思和温克获奖，1991年波尔和摩尔获奖。二等奖是里程碑奖，1983年给了王浩，1984年给了罗宾逊，1991年给了布莱索。一等奖被称为莱布尼茨奖（注意，这个和德国的那个莱布尼茨奖不同），一次也没发出过，因为条件是“不仅够格在数学杂志上发表，还要够格评选美国数学会的Cole奖或Veblen奖，甚至菲尔茨奖”。弗雷德金为计算机下棋设定的几个奖项有明确的标准：战胜特级大师，战胜当前世界冠军。按此标准就不难理解为什么马库恩的罗宾斯猜想尚不够格一等奖。沃思认为马库恩应该很接近了。但该奖的评委、哈佛数学家芒福德（David Mumford）想都不想地说：“现在不行，一百年都够呛（Not now, not 100 years from now）。”（Horgan，1993）随着定理证明事业的凋零，该奖后来也悄无声息地撤销了。也有乐观派，例如离散数学家格雷汉姆（Ron Graham3）认为在证明定理上计算机超过人是迟早的事，人脑毕竟是生物进化的产物，天生的目的不是用来证明定理的。吴文俊也算乐观派。

3他的太太是另一位成果丰富的离散数学家金芳蓉（Fan Chung）。

定理证明的过程，都是一个归约（reduce）的过程，无论是逻辑派的（即把数学问题归约到更基本的逻辑问题），还是形式派的（即用一套规则不断地变换给定的公式直到显性的形式出现）。自动定理证明研究这个数学过程的全自动化。但作为人的辅助工具，有时证明过程是人机互动的。波尔-摩尔证明器就允许人在证明过程中予以干预，例如增加一条引理等，尽管整个过程还是机器主导的。

1976年阿佩尔（Kenneth Appel）和黑肯（Wolfgang Haken）借助计算机证明了四色定理，他们把四色定理分成几种情况，其中的一些情况可以借助计算机枚举的方法予以证实或排查。这代表了另一类人机交互，即以人为主、计算机为辅的证明，也称为计算机辅助证明（computer assisted proof）。四色定理证明后，一些哲学家开始挑刺儿，王浩和普特南的学生铁木钦科（Thomas Tymoczko）提出了这样的问题：四色定理算被证明了吗？谁看见了这个证明过程？这听起来有点像乔姆斯基对统计派机器翻译的批评：有黑箱子的理解不能算理解，有黑箱子的证明也不能算证明。传统的数学实践遵循共同体过程，也就是一个数学家提出证明，然后一堆同一共同体的专家来验证，如果验证通过，定理成立，可能后面还伴随证明的改进。费马大定理的证明、庞加莱猜想的证明和张益唐的证明，都是这个套路。不独铁木钦科，很多数学家也持类似态度，毕竟这涉及自己饭碗的合法性。

四色定理被证明之后，又有越来越多的计算机辅助证明出现，这种现象在图论和组合数学中尤盛。1991年《图论杂志》（Journal of Graph Theory）的主编金芳蓉（Fan Chung）写信给所有编委讨论在什么条件下可以接受计算机辅助证明的论文。大家争论是否论文作者还应该提交计算机程序，而谁又来负责验证计算机程序的正确性。大家最后也没有得到明确的结论，传统的数学家们对计算机辅助证明总觉得有点不太舒服。

有些机器证明的定理本身并不长，例如罗宾斯猜想，人可以看得过来。而有些机器证明（无论是全自动的还是计算机辅助的）太长，人根本看不过来，例如布尔-勾股数问题（Boolean Pythagorean Triple Problem）的证明（2016年5月）一共有200TB，200TB的3D纯高清视频这辈子恐怕都看不过来，更甭说定理了。那怎么才算是证明了定理呢？我们退一步来看，如果那200TB文件可以用一个可被信任的计算机程序验证一遍，是不是就算是证明了呢？罗宾斯猜想的证明就曾用Mathematica验证过，而AUTOMATH本身就是一个验证系统。对全自动的定理证明，验证过程更容易机械化，而计算机辅助证明可能五花八门，很难有一个统一的过程。

其实不只是机器产生的证明会没心没肺地长，人证明的定理也会很长，相比有限单群分类定理的证明，庞加莱猜想的证明和张益唐的证明都不算什么了。这个证明涉及了大约100位数学家，近50年（1955年到2004年）的努力，论文分别发表在500个期刊上，总和超过了1万页。几位核心参与者正计划把证明编成12卷，已经出版了7卷。这更像是浩大的合作工程（mega engineering）项目。其间屡次发生错误和跳跃（gap），到今天也没有百分之百肯定的证明，因为整个证明涉及的社会复杂度。数学家所罗门（Ronald Solomon）专为此定理写过一个40页的简史。

无论如何，数学共同体的实践标准在变：从数学家之间互相核实到数学家信任的程序之间互相核实。理论物理学家温伯格（Steve Weinberg）在20世纪90年代的“科学大战” 中为科学实在论辩护时写过一篇《物理学与历史》的文章，批判他的“真理相对派”的对手们。他认为真理必须是客观的，而“后现代主义”的对手们的真理观认为真理是群体和文化的共识。但科学出版的同行评议（peer review）从某种意义上说就是共识，只不过共识的共同体是很小的内行，而不是全社会的投票民主。温伯格晚年专门研究物理学史，他认为外行不能替内行研究自己的历史。

也许在越来越复杂的数学证明中，需要引入某种机器证明的手段来增强我们人类对真理的信心。也难怪传统的数学家在抱怨：数学变成了有成本的实验科学。英国华威大学（Warwick）的数学教授爱波斯坦（David Epstein）办了本实验数学的杂志（Journal of Experimental Mathematics），被他的同行讥讽说应该叫“未证明定理杂志”。爱波斯坦不服，他指出前辈如高斯也利用过实验证明（Horgan，1993）。原来以为定理证明是最可解释的，因为每一步都有严谨的逻辑推理。但当我们面临一个有几百TB的证明，这恐怕比深度学习都更难解释，比深度学习学出来的黑盒子更黑。解释的工作必须是人做的吗？我们能够接受一个黑盒子对另一个黑盒子的解释吗？

其实那些典型的理化科学，例如物理、化学和生物学，是以实验为本的，可重复性（reproducibility）是检验真理的标准之一。只不过在当下，可重复性的成本太高。现在《自然》杂志上发表的那些生物学论文，又有多少是被重复过的？我们可以怀疑作者的诚信，我们也可以感慨，当下的数学变得越来越实验，而生物学可能变得越来越后现代了。可不是嘛，无论是唯心或唯理的数学，还是唯物或经验的实验科学，最终都成了共同体式的实用主义。

如果我们看看数学史，当解析几何刚出来时，很多传统的数学家并不认可解析几何的证明结果，认为相比欧几里得几何的证明过程，解析几何不算证明，因为它没有为被解决的问题提供真正的理解。

吴文俊和芒福德联合得了2006年的邵逸夫数学奖。对他们的得奖评语最后都有一句定论，大意是他俩都是从纯数学的分支拓扑最后转到和计算机科学相关的研究，这为数学家的未来行为模式提供了一种典范。吴文俊声称他的几何定理证明的思路来自中国古代数学思想，他认为丝绸之路使得中国和中亚交流密切，花剌子模4的数学思想也必定和中国古代数学思想互有渗透。这可能有点拔高中国数学了。吴文俊曾留学法国，法国的数学家素有关心数学史的传统，和吴文俊相识的人中阿达玛（Jacques Solomon Hadamard）5和布尔巴基学派的丢东聂（Jean Alexandre Eugène Dieudonné）也都是数学史家。吴文俊的结论是中国数学是巴比伦式的而不是希腊式的，巴比伦数学讲究计算，而希腊数学讲究公理。其实印度和阿拉伯数学也都是讲计算的。

4花剌子模：中亚西部地名，现属乌兹别克斯坦，算法一词Algorithm源于al-Khwarizmi，即指花剌子模。

5Hadamard也译为“哈达玛”，发音更接近“阿达玛”。

自动定理证明依靠的工具是计算机，正是计算模糊了理性和经验的边界。可以登高一步说：计算是知识演化的基础，也是知识民主化的工具。阿达玛曾经研究过数学的心理学，我们无法套用他的很多老套说法。但观察和计算机科学相关的数学家：机器定理证明的开拓者之一沃思是盲人，他专攻逻辑；而麦卡锡尽管在人工智能中走了逻辑这一条路，但他在普林斯顿大学的博士导师却是失去双手的拓扑学家莱夫谢茨。数学家某些感官的缺失会影响到他们不同的数学能力吗？这对他们选择不同的主攻方向会有影响吗？有人说数学家都喜欢艺术尤其是音乐，我们不知道是逻辑学家更喜欢音乐，还是拓扑学家更喜欢音乐。

阿贡实验室的定理证明小组2006年被裁掉了，这大概算是符号派低潮的标志性事件。这一年辛顿（Geoffrey Hinton）的深度学习论文发表在《科学》杂志上。一个时代结束了，另一个时代开启。对定理证明做出巨大贡献的马库恩失业了，他那时还不到53岁，一年后他走投无路去了新墨西哥大学担任没有终身教职的研究教授。他离开阿贡后无法对Otter做大的改进，Prover9是他的新证明器的构想，但没时间得到完美的实现，Otter/Prover9的性能遂被其他团队逐渐超越。目前最领先的一阶逻辑定理证明器是曼彻斯特大学的“吸血鬼”。2011年马库恩因急症去世。他在阿贡的前老板沃思深情地写了一篇纪念文章，沃思提到当年在阿贡时，马库恩的狗得了癌症，兽医给了马库恩两个选择：化疗或安乐死，他选择了后者。

有些领域，一开始就把百分之八十的容易问题解决了，而后就一直很难，进展很慢，少有突破。人工智能就是这样，定理证明尤其如此。深度学习领域近来的进步更多得益于硬件。而定理证明，即使硬件再发达很多，也还没有看到曙光。

定理证明是极端的符号派。所有符号派的人工智能技术的基础都是定理证明，如专家系统、知识表示和知识库。甚至关系数据库，如果加上递归，也被证明等价于没有函数的一阶逻辑。专家系统的很多术语其实是重新包装过的定理证明术语。例如“知识库”就是“公理集合”，“规则库”就是“支持集”，“推理引擎”更是直接照搬。当下流行的（或马上要流行的）知识图谱的基础也是定理证明技术——知识表示的理论“描述逻辑”就是被约束的一阶逻辑的子集。

按照数学哲学的分类，如果说基于逻辑的定理证明技术是逻辑主义的延伸的话，以项重写技术为基础的计算机代数无疑是形式主义的精神遗产。定理证明领域的名字也经历了有趣的演化。最早都叫机器定理证明（Mechanical Theorem Proving），后来改叫自动定理证明（Automatic Theorem Proving），再后来叫自动演绎（Automated Deduction），目前都叫自动推理（Automated Reasoning）。原因很简单，演绎（deduction）只是推理的一种，现在归纳（induction）、溯因（abduction）也都算成推理了。贝叶斯推理，可以叫Bayesian Logic，或Bayesian Inference，也可以叫Bayesian Reasoning。最早的定理证明国际会议（CADE，The International Conference of Automated Deduction）开始是每两年一次，1996年之后改为每年一次，但奇数年都是自己开，而偶数年是和其他几家计算机科学相关的逻辑会议一起开，叫IJCAR（International Joint Conference of Automated Reasoning）。这促成了自动定理证明圈子和人工智能圈子的融合。定理证明的几个主要会议的会议记录原来都被斯普林格出版社收入到计算机科学讲义（LNCS）系列，现在也都归到人工智能讲义（LNAI）系列了。

如果我们用谷歌Ngram来看看1960年到2008年间的定理证明发展会觉得很有意思。“自动定理证明”（Automated Theorem Proving）明显在逐渐被“自动演绎”（Automated Deduction）和“自动推理”（Automated Reasoning）所取代，而“计算机代数”和“自动演绎”的流行度差不多。即使是一个很偏门（至少是曾经很偏门）的“强化学习”（Reinforcement Learning），在2000年后也要远比“自动推理”流行得多。Ngram目前只开放到2008年，那时还没有现在已经如日中天的“深度学习”。

自动定理证明与强化学习

有意思的是，最近有人开始把深度神经网络应用到定理证明中。一阶逻辑证明中的一个难题是如何从已经证明的子句集合中选取下一个子句，这会极大地影响定理证明器的后续表现。一个谷歌团队的实验表明，简单的卷积网络可以帮助定理证明器挑选子句从而提高性能（Loos，2017）。

王浩曾经抱怨数学家不把逻辑学家当回事。图灵也有类似的说法：逻辑学家给数学家提供了有营养的饭菜，但做得不够美味，数学家不爱吃。曾几何时，王浩建立的洛克菲勒大学王实验室（Wang Lab）6在鼎盛时期网罗了当时逻辑学界的所有重要人物（如克里普克、DA马丁等），俨然是逻辑学的中心，连王浩的老师蒯因也一度想加盟。但在20世纪80年代，洛克菲勒大学因为经费原因裁减了所有唯心的实验室（包括数学和逻辑学），逻辑实验室只剩王浩一个光杆司令。

6洛克菲勒大学是医学与生物学重镇，学校只培养博士，不设系，每个教授有自己的实验室。

按照知识的“食物链”，生物学家不敢怠慢化学家，化学家不敢怠慢物理学家，物理学家不敢怠慢数学家。乔姆斯基也说过类似的话：物理不好解的问题就升级到化学，化学解不了的就再升级到生物学。在《大英百科》的Propedia卷中，知识链条依次被列为：逻辑，数学，科学，历史与人文，哲学。也就是说，数学上面是物理，再上面是化学，再上面是生物，等等。但大多数数学家不认为他们应该利用逻辑作为工具。数学家背上码了一摞乌龟，但他们却说我们肚子底下啥也没有7。

7“乌龟背上有乌龟”（turtles all the way down），是认识论的一个说法。

维特根斯坦曾有言：“逻辑似乎处于一切科学的底部——因为逻辑的研究探索一切事物的本质。”但数学家不觉得他们非得趴在逻辑学家的背上。解决了希尔伯特第十问题的几位逻辑学家和计算机科学家并没有被数学共同体认可，也没得过什么数学大奖。自动定理证明的状况与此相关，数学家没觉得这玩意儿有用，人工智能的两派人马都不待见。再过几年，可能就没什么人能教“自动定理证明”的课了。

哈尔莫斯（Paul Halmos）是数学家，但也曾涉猎逻辑，还出过一本《朴素集合论》（Naive Set Theory），是同类书中销量最好的。哈尔莫斯在自传里拿逻辑开玩笑，说即使有人证明了黎曼猜想是不可判定的（哥德尔就是这么猜测的），数学家睡一觉，第二天起来还是该干吗干吗，仍不睬逻辑。他还说数学家才不关心量词顺序是∀∃还是∃∀，这明显是在轻浮地调侃王浩。他也许不知道现在NP问题是克雷研究所最关心的千禧年数学问题。哈尔莫斯是1957年康奈尔大学逻辑大会的组织者之一，他的自传不无自嘲地引用了大会文集结束语的打油诗：

如果你的文章内容太稀，

就用一阶函数来凑齐。

然后它就成了逻辑，

似乎施了魔法把功吸。

本来平常稀松的东西，

立马变成被人欢呼的奇迹。

所有定理证明系统（无论是逻辑主义的还是形式主义的）的一个致命问题是它们多是独立的，很少和其他数学工具结合，结果必然是只能是玩具系统，而不具实用性。就像早期的计算尺、手摇计算器等原始计算工具一样，目前的各种计算辅助数学工具（例如Mathematica）的主要用户并不是数学家，而是物理学家和工程师。更广义地说，整个人工智能领域都有同样的问题：子系统和子领域之间没什么联系，鲜有整合。

必然性（necessity）和可能性（possibility）是相对的。底层的必要性约束了上层的可能性。物理定律的可能性被更底层的数学定理的必然性所约束；依次，数学定理的可能性又被逻辑的命题和定义所约束。上层的思想（thought）恰是底层的世界（world），一类人的思想是另一类人的世界。

数学是人类智力的最高端。不明就里的哲学家对数学说三道四是令人最不能忍受的。曾有哲学家怀疑数学真理的必然性，理由是数学家在自己的著作中也常用“也许”“可能”之类的词汇。逻辑学家霍奇斯（Wilfrid Hodges）曾撰文《数学中的必然性》（Hodges，2007）对这些非逻辑学家出身的哲学家表示不满。他统计了著名的代数教科书（伯克霍夫和马克雷恩的《现代代数研究》）的头一百页中出现的所有模态词（allow, can, cannot, could, essential, have to, impossible, inevitably, may, might, must, necessarily, need not, need only, possibility, possible, will），一共340次，平均每页3.4次。但这些模态词都是修辞，而不是语义。

逻辑要想有用，必须走定理证明的路子，当所有的数学家都离不开定理证明器时，逻辑学家才敢对趴在背上的数学家和数学家背上的那谁以及更上的那谁理直气壮。法国数学物理学家吕埃勒（David Ruelle）在庆祝薛定谔数学物理研究所成立20周年的发言题目叫“后人类数学”（Post-Human Mathematics）。他说也许某一天，我们人类看机器做数学，就像黑猩猩看我们阅读伽罗瓦理论。其实这在机器下棋里已经发生了，两个Alpha-zero下棋，我们人类已经看不懂了，从这个意义上说，定理证明比下棋可难多了。

除了几本教科书和那本手册，Siekmann和 Wrightson编辑的经典论文集Automation of Reasoning是不错的参考文献。如果懂一点逻辑，想进一步探索，可参考王浩的《数理逻辑通俗讲话》，其中提到了机器定理证明和计算理论，虽然书是1981年出版的，但对于深度科普而言，不算过时。

戴维斯的The Early History of Automated Deduction（Davis，2001）和白贝尔的Early History and Perspectives of Automated Deduction（Bibel，2007）是自动定理证明早期历史的第一手材料。Tarski's Influence on Computer Science（Feferman，2005）澄清了塔尔斯基对于自动定理证明的态度。20世纪80年代末期出版的《人工智能手册》中有两章关于机器定理证明的内容，但取材莫名其妙，想想手册的编者是费根鲍姆一干人等，也就不会太过惊奇。

如果觉得只看文献不过瘾，真起了兴，还想动动手，不妨看看Riazanov的博士论文。Riazanov是沃伦可夫（Andrei Voronkov）的学生，师徒俩合作了高效的“吸血鬼”定理证明器，在相当长一段时间内，“吸血者”都是一阶逻辑定理证明大赛的冠军。对实战者而言，项索引不可不懂，Term Indexing（Graf，1996）是这方面有益的参考书，尽管内容略有些过时，其中对几种索引算法效率的比较标准也被人质疑。

微软的早期核心员工查尔斯·西蒙尼（Charles Simonyi）1995年为牛津大学捐了一个科普教授席位Simonyi Professor of Public Understanding of Science，第一位担任这个讲席的是生物学家、无神论者道金斯（Richard Dawkins），接替道金斯的是数学家索托伊（Marcus du Sautoy）。关于机器和数学家的关系，索托伊在他的科普书《天才与算法：人脑与AI的数学思维》（The Creativity Code: Art and Innovation in the Age of AI）中讲了几个有趣的故事。既然物理学家可以用望远镜，生物学家可以用显微镜，数学家为什么不能用机器来帮帮忙呢。

吴文俊的生平见吴文俊《走自己的路》。王浩的生平见尼克《哲学评书》和齐河县政协文史资料委员会编《齐河文史资料第六辑》。

自动定理证明领域的大奖以埃尔布朗（Herbrand，或译厄布朗，国内也有按英文发音译为赫尔布兰德）命名。埃尔布朗是天才的法国数学家，他的博士论文为数理逻辑的证明论和递归论奠定了基础。当哥德尔不完全定理刚出来时，他检查了自己的论文，写了一句话作为附言：哥德尔的结果和我的结果并不矛盾。他给比他年长两岁的哥德尔写信讨论递归函数，哥德尔1931年7月25日给他回了信，两天后埃尔布朗爬阿尔卑斯山时因事故身亡，年仅23岁。一阶逻辑证明中的埃尔布朗域（Herbrand Universe）以他命名。沃思是当之无愧的第一届得奖人，吴文俊是第四届，马库恩是第七届。2015届是“吸血鬼”的作者、曼彻斯特大学教授沃伦可夫。2016届是以时态逻辑做程序证明的斯坦福大学退休教授马纳和斯坦福研究所（SRI）的瓦丁格。2017届获奖者保尔森（Lawrence Paulson）是高阶逻辑证明的领袖人物，同时也是函数程序语言ML的主要提倡者，他也是少有的在美国受教育到英国工作的人，他在斯坦福大学的博士导师是和理论与逻辑不沾边的John Hennessy。2018届的奖对得奖人布赫伯格（Bruno Buchberger）来说是迟到的，他的计算机代数的贡献是开创性的。

本书除了梳理历史，还想有科普的功能。理论上说，如果有一本好的教科书，就不需要依赖原始文献了——想了解牛顿第二定律不一定非得读牛顿写的《自然哲学的数学原理》。但自动定理证明学科恰缺乏合适的教科书。早期最有影响的教科书当属Symbolic Logic and Mechanical Theorem Proving（Chang，Lee，1973），书的两位作者20世纪60年代末在加州大学伯克利分校读博士时是同学，那时正是定理证明发展的高峰期。作者之一Lee就是李家同（Richad Char-tung Lee），他的曾祖父李瀚章是李鸿章的长兄。李家同后来回到中国台湾做了“清华大学”代理校长和“暨南国际大学”校长，也是成功的散文作家。这本书的整体风格非常好，而且有大量习题，无论教学还是自学皆可。但书中第7章存在几个致命的错误，否则真可以成为本领域的经典。本书的另一作者Chang则一直待在美国，长期在IBM工作，后来又写了一本人工智能的教科书，但再无大名。两位作者的不同境遇可作为留学生选择海归还是留美的参照。后来两位都远离定理证明领域，该书也没再出修订版，很可惜。

Automated Theorem Proving: A Logical Basis（Loveland，1978），风格与Symbolic Logic and Mechanical Theorem Proving类似，更严格，但内容业已老化。

Automated Theorem Proving 1965–1970（Wos，1983）是一本很容易读的书，但很少讲逻辑和定理证明技术的原理，更像是阿贡实验室早期定理证明器的使用手册。阿贡系作者的所有书都有类似的特点。

Automated Theorem Proving（Bibel，1987）虽是教科书体例，但内容偏重作者自己的连接方法，目前已不是主流。

Logic for Mathematics and Computer Science（Burris，1997）主要是逻辑的教科书，但书中专有一章讲方程逻辑，详细地讲解了Knuth-Bendix过程，是方程逻辑和项重写很好的入门材料。

Logic for Applications（Nerode，Shore，1997）的两位作者都是逻辑学家。整体内容严谨。缺憾是比较偏重Prolog，定理证明的技术只讲了线性归结。

Logic for Computer Science: Foundations of Automatic Theorem Proving（Gallier，2003）的体例很像Logic for Applications，讲过归结后讲了SLD归结，这是Prolog的理论基础。这两本书我更喜欢Logic for Applications。

First-Order Logic and Automated Theorem Proving（Fitting，1995）也是一本入门书，讲了归结，也讲了表方法（Tableaux）。作者是埃尔布朗奖得主。

Handbook of Automated Reasoning（Robinson，Voronkov，2001）是手册型。两位编者一位是归结原理的发明者，另一位是目前最厉害的定理证明器“吸血鬼”的主要作者。内容现代、完整。但不是教科书形式，初学者读起来会很费劲。

不过话说回来，如果现在非要我推荐一个定理证明教科书的作者，Voronkov应该是第一人选。好的教科书的缺乏也反映了这个学科的凋零。至于进一步的学习，不严肃的读者看完本章就可以打住，看多了耽误您前程。严肃的读者可先从Logic for Applications下手，然后看看Logic for Mathematics and Computer Science方程逻辑那一章，对个别议题感兴趣的再去看Handbook of Automated Reasoning。

上一章目录下一章