人工智能名人堂第40期 | 归结原理创始人：约翰·罗宾逊

2017 年 8 月 14 日 德先生

丘吉尔曾说过，“The longer you can look back, the farther you can look forward. (回顾历史越久远，展望未来就越深远)”，为纪念人工智能领域做出杰出贡献的先辈与开拓者们，鼓励更多后起之秀投身该领域，人工智能国际杂志《IEEE Intelligent Systems》自2006年始至今陆续推选出了60位人工智能专家(参看《诺伯特·维纳奖得主王飞跃 | AI 名人堂，世界人工智能60年60位名人榜》)。德先生自2016年10月31日起，已定期于每周一在微信公众号（D-Technologies）上发布人工智能名人堂60位成员的相关介绍。往期内容可查看延伸阅读。

约翰·罗宾逊（John Alan Robinson，1930年3月9日- 2016年8月5日）是世界著名的哲学家、数学家和计算机科学家，同时在雪城大学担任名誉教授。

约翰·罗宾逊的主要贡献是奠定了自动定理证明的基础。他提出的通代算法消除了在解析证明中组合性爆炸一个来源，同时也奠定了逻辑编程的范式，特别是Prolog语言。罗宾逊因在自动推理中的杰出贡献获得了1997年Herbrand自动推理杰出成就奖。

代表作有：

Handbook of Automated Reasoning (2001)

Natural and Artificial Parallel Computation（1990）

Logic: Form and Function （1979）

A Machine-Oriented Logic Based on the Resolution Principle （1965）

人物生平

约翰·罗宾逊1930年出生于英国约克郡，1952毕业于剑桥大学，获古典文学学士学位，并于同年来到美国。来到美国后，约翰·罗宾逊在俄勒冈大学学习哲学，之后就读于普林斯顿大学，并在1956年获得哲学博士学位。

毕业后，约翰·罗宾逊进入杜邦公司担任业务研究分析师，在此期间他自学了编程以及数学。1961年，约翰·罗宾逊进入莱斯大学，利用暑假时间在阿贡国家实验室应用数学部担任客座研究员。1967年，约翰·罗宾逊成为雪城大学的逻辑学和计算机科学特聘教授，1993年获得荣誉教授称号。

在阿贡国家实验室，约翰·罗宾逊对定理机器证明以及消解和统一原理表现出了浓厚的兴趣。在许多定理机器证明系统中包含了消解与统一，是逻辑编程和编程语言Prolog中推理机制的基础。

约翰·罗宾逊是《Journal of Logic Programming》的创办编辑，一生获得了许多荣誉，包括1967年古根海姆奖（Guggenheim Fellowship）；1985年因自动定理证明获得美国数学学会里程碑奖（American Mathematical Society Milestone Award）；1990年当选美国人工智能学会（AAAI）会士；1995年获得洪堡特高级科学家奖（Humboldt Senior Scientist Award）；1997年因在自动定理证明的杰出贡献获得Herbrand自动推理杰出成就奖；1997年，逻辑编程协会授予约翰·罗宾逊逻辑编程创始人荣誉称号。1988年，约翰·罗宾逊获得比利时鲁汶大学荣誉博士学位，1994年获得乌普萨拉大学荣誉博士学位，2003获得马德里理工大学荣誉博士学位。2016年8月5日，因胰腺癌手术后动脉瘤破裂，约翰·罗宾逊在美国波特兰去世。

归结原理简介

归结原理又被称为归结法则、分解法则、消解法则。使用这种方法时，对任一要证明的永真公式取非后，证明它不可满足，为此先转化成一种标准型，然后对这个标准型不断使用单一的推理规则，即实行归结，直到导出矛盾。

由谓词公式转化子句集的过程可以了解到：子句集中的子句之间是合取关系，其中只要有一个子句不可满足，则子句集就不可满足。另外，空子句是不可满足的。因此，若一个子句集中包含空子句，则这个子句集一定是不可满足的。Robinson归结原理就是基于这一认识提出来的。其基本思想是：检查子句集S中是否包含空子句，若包含，则S不可满足；若不包含，就在子句集中选择合适的子句进行归结，一旦通过归结能推出空子句，就说明子句集S是不可满足的。

命题逻辑

在命题逻辑归结原理的推理图式中，P、Q和R称为原子公式（简称原子），即不使用逻辑连接词的简单命题形式。原子和原子的否定式统称句元，例如P与塡P、Q与塡Q、R与塡R即是三对互补句元。子句就是将不同句元用析取词∨（或）连接而成的析取式。应用归结法则进行推理时，所有判断都写成子句的形式，这不论对命题逻辑还是对一阶谓词逻辑都不例外。

在命题逻辑中，原子被看成一个内部结构不予分析的逻辑基元，代表简单的命题形式。单凭普通形式逻辑中充分条件的假言联锁推理的符号化，只能直接演变为命题逻辑的归结原理。命题逻辑的归结原理或归结法则可归纳如下：对任意两个子句H1和H2，如果H1和H2中各自包含一个互补的句元L1和L2（例如上述图式中的Q和塡Q），则可以删去L1和L2，并将原来的子句H1与H2归结为删去互补句元后两子句余下部分的析取式C。C也以子句形式出现，称为原来两子句（常称为亲子句）的一个归结式例如图式中塡P∨R即为塡P∨Q与塡Q∨R两子句的一个归结式。归结原理或归结法则即因此得名。

基本思想

从应用的角度出发，可以从充分条件的假言联锁推理、命题逻辑的归结原理，一阶谓词逻辑的归结原理等三个方面来分析归结原理的基本思想。

充分条件的假言联锁推理是前提和结论全部由充分条件假言判断构成的一种推理形式。下面是普通形式逻辑中在引入蕴涵连接词“→”（代表如果……则……的逻辑关系）后的推理图式：

归结原理

横线上、下方的逻辑公式分别与推理的前提和结论相对应。

由于P→Q (如果P 则Q)和归结原理（非P或Q）这两个公式逻辑等价，即（P→Q）呏（塡P∨Q）,同理有（Q→R）呏（塡Q∨R）,（P→R）呏（塡P∨R）。用这些逻辑等价关系的右式分别替换其中的蕴涵公式，即得命题逻辑中使用归结法则的推理图式：

归结原理

在命题逻辑归结原理的推理图式中，P、Q和R称为原子公式(简称原子),即不使用逻辑连接词的简单命题形式。原子和原子的否定式统称句元，例如P与塡P、Q与塡Q、R与塡R即是三对互补句元。子句就是将不同句元用析取词∨（或）连接而成的析取式。应用归结法则进行推理时，所有判断都写成子句的形式，这不论对命题逻辑还是对一阶谓词逻辑都不例外。

一阶谓词逻辑

一阶谓词逻辑中，原子是由谓词和项组成的，因而在句元和子句中就有个体变元出现。由于存在量词能用斯科林变换消去，可以认为句元和子句中的个体变元只受全称量词约束。

两个子句H1与H2的归结式可分四种情形:①子句H1与H2的归结式;②子句H 1与子句H2的因子句H2′的二元归结式；③子句H 1的因子句H1′与子句H2的二元归结式；④子句H1、H2各自的因子句H1′与H2′的二元归结式。

求子句的因子句和求两子句归结式时,都必须用合一算法求出最普遍合一替换MGU（most general unifier）,或称最广通代。这是在一阶谓词逻辑中应用归结法则的关键技术，最普遍合一替换是在一个表达式集合E={E1,…，Ek}中,用一组项（t1,…,tk）替换一组互异个体变元（x1,…,xk）,使替换后的各表达式相等（称为合一）的最简替换。①求子句因子句时的最普遍合一替换：例如子句H1＝P(x)∨P(f(y))∨塡Q(x) 的因子句H1′＝P(f(y))∨塡Q(f(y))，mgu={f(y)/x}。②求两子句（包括子句之一或两子句都有因子句的情形）的二元归结式时的最普遍合一替换:例如子句H 2=塡P(f(g(a))∨R(b),则H2与上例H1的因子句H1′的二元归结式C =塡Q(f(g(a))∨R(b),mgu={g(a)/y}。

应用方法

应用归结原理证明定理或求解问题时采用反证法，即先假设与结论相反的命题是成立的，然后根据前提和否定结论的假设（都以子句形式出现），求出一系列中间结论（以归结式的形式出现），如果最后得到两个相互矛盾的命题（以互补句元形式出现的一对单句元子句），即表明与结论相反的假设不能成立，因而原结论的正确性得证，此时归结式是空子句□。可以从理论上证明一阶谓词逻辑的归结原理是完备的，即一个子句集S(前提和结论否定式合取形成的全体子句)不可满足的充要条件是从子句集S 中能推导出空子句。

约翰·罗宾逊提出的归结方法，使得自动定理证明领域发生了质的变化。建立在Herbrand定理之上的归结原理比起Herbrand定理有重大改进，既节约了很多时间和空间，又使自动定理证明变成了现实，不仅推动了自动定理证明这一课题的发展，还促进了麦卡锡使用逻辑来建造最终的意见接受者的计划。基于谓词逻辑的归结原理是广泛应用于人工智能和计算机科学中的一种理论知识，为人们解决实际生活中的一些问题提供了有力的帮助。