今年修了四川大学潘无名老师的「AI面向语言编程」课程，这门课程的期末论文要求对SLD消解进行简单叙述，因此我对相关内容进行了粗浅的学习。

此篇为关于SLD消解的学习笔记，简略介绍了SLD消解的原理和思想。

因为时间比较紧张，故没有仔细斟酌行文结构、语法、语言流畅度，读起来十分缺乏user-friendliness，以后如果有时间，会试图讲得更详细、明白些的。

Prolog 程序的执行过程是一个（归结）演绎推理过程。其推理方式为反向推理，控制策略是深度优先且有回溯机制，具体实现方法是：自上而下匹配子句；从左向右选择子目标；（归结后）产生的新子目标总是插入被消去的目标处（即目标队列的左部）。

SLD 消解是 Prolog 程序的运行机理，也就是所谓的 Prolog 语言的过程性语义。

SLD Resolution

消解法是命题逻辑完备且充分的算法：当且仅当算法报告其不可满足时，分词形式的公式是不可满足的。对于命题逻辑，该算法也是不可满足的决策过程，因为它保证终止。当推广到一阶逻辑时，消解仍然是完备的，但它不是一个决策过程，因为算法可能不会终止。[3]

消解法最初是作为自动定理证明的方法而开发的。后来，发现受限形式的消解法可以被用来通过编程来实现计算，这种方法称为逻辑编程( logic programming )。程序表示为一组子句，查询表示为可以与一个或多个程序子句冲突的附加子句，先假设与结论相反的命题是成立的，然后根据前提和否定结论的假设（都以子句形式出现），求出一系列中间结论（以归结式的形式出现），如果最后得到两个相互矛盾的命题（以互补句元形式出现的一对单句元子句），即表明与结论相反的假设不能成立，因而原结论的正确性得证，此时归结式是空子句 $\square$ 。可以从理论上证明一阶谓词逻辑的归结原理是完备的，即一个子句集 $S$（前提和结论否定式合取形成的全体子句）不可满足的充要条件是从子句集 $S$ 中能推导出空子句。[4]

而下面将要讨论的SLD Resolution，就是一种满足上述所描述的，适用于逻辑编程的归结方法之特性的优化归结策略。

SLD Resolution简介

SLD 消解(Selective Linear Definite clause resolution / Linear Resolution with Selection function for Definite Clause) 又叫SLD 归结，是一种完备的、充分的消解策略，它基于Horn子句，是完备( complete )且充分( sound )的。

SLD 消解源自Robert Kowalski提出的一种未命名的推理规则[1]，后来由Maarten van Emden取名为 SLD 消解。这个名字来自SL 消解[2]——一种通过不受限制的子句形式进行推理的消解方法，“SLD”是对SL 消解的改进，相较于SL 消解，SLD 消解通过明确的子句——Horn子句——进行消解。

“SL”和”SLD“中”S“，代表着要被消解的文字( literal )是通过一种选择规则( selection rule )从$C_i$子句中选出来的。在SL 消解中，被选中的文字由一种特定的规则选择，比如说：先进先出规则，即依照一系列子句的书面顺序进行选择。但在SLD 消解中，选择规则更加泛化，没有严格的规则限定如何选择文字。

SLD 消解被运用在Prolog 中，SLD 消解是 Prolog 程序的运行机理，也就是所谓的 Prolog 语言的过程性语义。Prolog 程序的执行过程是一个（归结）演绎推理过程。其推理方式为反向推理，控制策略是深度优先且有回溯机制，具体实现方法是：自上而下匹配子句；从左向右选择子目标；（归结后）产生的新子目标总是插入被消去的目标处（即目标队列的左部）。

接下来我们将详细介绍SLD 消解的原理与思想。

SLD Resolution基础

一阶谓词逻辑

个体词、谓词、量词

个体词

个体词是指所研究对象中可以独立存在的具体的或抽象的客体。

将表示具体或特定的客体的个体词称作个体常项，一般用小写英文字母 $a, b, c…$ 表示；而将表示抽象或泛指的个体词称为个体变项，常用 $x, y, z…$ 表示。称个体变项的取值范围为个体域(或称论域)。

个体域可以是有穷集合，例如，${1，2，3}，{a，b，c，d}，{a，b，c，…，x，y，z}，…$；也可以是无穷集合，例如，自然数集合 $N={0，1，2，…}$ ，实数集合 $R={x|x是实数}$。

有一个特殊的个体域，它是由宇宙间一切事物组成的，称它为全总个体域。

谓词

谓词是用来刻画个体词性质及个体词之间相互关系的词。同个体词一样，谓词也有常项和变项之分。表示具体性质或关系的谓词称为谓词常项，表示抽象的、泛指的性质或关系的谓词称为谓词变项。无论是谓词常项或变项都用大写英文字母 $F，G，H，…$ 表示，可根据上下文区分。

量词

有了个体词和谓词之后，有些命题还是不能准确的符号化，原因是还缺少表示个体常项或变项之间数量关系的词。称表示个体常项或变项之间数量关系的词为量词。量词可分两种:

• 全称量词

日常生活和数学中所用的“一切的”，“所有的”，“每一个”，“任意的”，“凡”，“都”等词可统称为全称量词，将它们符号化为 $\forall$ 。

• 存在量词

日常生活和数学中所用的“存在”，“有一个”，“有的”，“至少有一个”等词统称为存在量词，将它们都符号化为 $\exists$。

谓词公式

定义1

1)常量符号是项；

2)变量符号是项;

3)若$f(x_1,⋯,x_n)$是n元函数符号，$t_1,⋯,t_n$是项，则$f(t_1,⋯,t_n)$是项；

4)所有项都是有限次使用1),2),3)生成的符号串。

定义2

若$P(x_1,⋯,x_n)$是n元谓词符号，$t_1,⋯,t_n$是项，则$P(t_1,⋯,t_n)$是原子

定义3

1)原子是公式；

2)若$G，H$是公式，则$(¬G),(G∨H),(G∧H),(G→H),(G↔H)$是公式；

3)若$G$是公式，$x$是$G$中的自由变量，则$∀xG,∃xG$是公式；

4)所有公式都是有限次使用1),2),3)生成的符号串

定义4

谓词逻辑中公式$G$的一个解释$I$，是由非空区域$D$和对$G$中常量符号，函数符号，谓词符号以下列规则进行的一组指定组成：

1.对每个常量符号，指定$D$中一个元素；

2.对每个$n$元函数符号，指定一个函数，即指定$D^n$到$D$的一个映射；

3.对每个$n$元谓词符号，指定一个谓词，即指定$D^n$到${0,1}$的一个映射。

定义5

公式$G$称为可满足的，如果存在解释$I$，使$G$在$I$下取1值，简称$I$满足$G$。若$I$不满足$G$，则称$I$弄假$G$。

定义6

公式$G$称为是恒假的(或不可满足的)，如果不存在解释$I$满足$G$；公式$G$称为恒真的，如果$G$的所有解释$I$都满足$G$

归结演绎推理

子句集

定义1 原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句。

定义2 对谓词公式G，通过以下步骤所得的字句集合S，称为G的子句集。

1. 消去蕴涵词和等值词。
2. 缩小否定词的作用范围，直到其仅作用于原子公式。
3. 适当改名，使量词间不含同名指导变元和约束变元。
4. 消去存在量词。
5. 消去全称量词。
6. 化公式为合取范式。
7. 适当改名，使子句间无同名变元。
8. 消去合取词，以子句为元素组成一个集合S。

定理1 谓词公式G不可满足 iff G的子句集不可满足。

定义3 子句集S是不可满足的，当且仅当其全部子句的合取式是不可满足的。

命题逻辑中的归结原理

归结演绎推理是基于一种称为归结原理的推理规则的推理方法，归结原理由J.A.Robinson于1965年首先提出，是谓词逻辑中一种机械化推理方法，归结原理的出现，被认为是自动推理，特别是定理机器证明领域的重大突破。

定义4 设$L$为一个文字，则称$L$与$\neg L$为互补文字。

定义5 设$C_1$、$C_2$是命题逻辑中的两个子句，$C_1$中有文字$L_1$，$C_2$中有文字$L_{2}$，且$L_{1}$与$L_{2}$互补，从$C_1$、$C_2$中分别删除$L_{1}$、$L_{2}$，再将剩余部分析取起来，记构成的新子句为$C_{12}$，则称$C_{12}$为$C_1$、$C_2$的归结式（或消解式），$C_1$、$C_2$称为其归结式的亲本子句，$L_{1}$、$L_{2}$称为消解基。

定理2 归结式是其亲本子句的逻辑结论。

由以上定理可以得到，用消解原理可以代替其他所有的推理规则，这个方法为机器推理提供了方便。

替换与合一

定义6 置换是一个形如${t_1/v_1,…, t_n/v_n}$的有限集,其中每个$v_i$是变量,$t_i$是不同于$v_i$的项（常量、变量或函数）$(v_i\neq t_i)$. 当$i\neq j$时，$v_i\neq v_j$，无元素组成的置换称为空置换, 记为$\varepsilon$。

其中，被置换元素必是变量，置换元素是项；置换元素必不同于被置换元素；在一次置换中，针对同一元素的置换只能出现一次(单次置换的同时性)；无元素组成的置换，成为空置换。

定义7 $\theta$是一个置换，E是一个表达式，Eθ称为E的实例(instance);

定义8 $E_1θ=…=E_nθ$, 则称置换θ为${E_1,…,E_n}$的合一子(unifier). 如果对${E_1,…,E_n}$存在这样的合一子, 则称集合${E_1,…,E_n}$可合一.

定义9 如果对E的每个合一子θ, 都存在一个置换λ, 使得θ=γ°λ, 则称合一子γ是集合${E_1,…,E_n}$的最一般合一子(most general unifier，mgu)

如果能够找到一个公式集的合一，特别是最一般合一，则可使互否的文字的形式结构完全一致起来，进而达到消解的目的。

谓词逻辑中的归结原理

定义10 设$C_1$、$C_2$是两个无相同变元的字句，$L_1$、$L_2$分别是$C_1$、$C_2$中的两个文字，如果$L_1$、$L_2$有最一般合一$\sigma$，则子句$(C_{1} \sigma - { L_{1} \sigma }) \cup (C_{2} \sigma - { L_{2} \sigma })$称作$C_1$、$C_2$的二元归结式（二元消解式），$C_1$、$C_2$称作归结式的亲本子句，$L_1$、$L_2$称作消解文字。

定理3 谓词逻辑中的消解式是它的亲本子句的逻辑结果。

由此定理我们即得谓词逻辑中的推理规则：

$$C_{1} \wedge C_{2} => (C_{1} \sigma - { L_{1} \sigma }) \cup (C_{2} \sigma - { L_{2} \sigma })$$

此规则称为谓词逻辑中的消解原理（归结原理）。

定理4 （归结原理的完备性定理）如果子句集S是不可满足的，那么必存在一个由S推出空子句$\square $的消解序列。

归结策略

归结原理如何在机器上实现？下面给出一个一般性算法：

Input: 子句集 $S$。
Output: $S$ 是可满足的或不可满足的。

让S成为子句集并定义 $S_0 =S$.

重复以下步骤从$S_i$得到$S_{i+1}$ 直到过程结束：

• 取一对之前未选过的互斥子句 ${C_1,C_2}⊆S_i$

• 根据归结原理，计算 $C = Res(C1, C2) $
  $S_{i+1} = S_i ∪ {C}$

结束算法，当：

• $C=2$。

• 所有互斥对都已经消解。

可以看出，一般性归结算法使用穷举法归结，问题在于，对于一个规模较大的实际问题，其开销将非常大——这种方法会产生许多无用的子句，这样，随着归结的进行，子句集会变得越来越大，以至于机器不能容纳，同时，归结的时间消耗也非常巨大。

因此，可以采用归结策略来优化归结算法，这些归结策略有：

• 删除策略
• 支持集策略
• 线性归结策略
• 输入归结策略
• 单元归结策略

SLD消解就是一种线性归结策略，故接下来将详细讨论线性归结策略。

线性归结策略

在归结过程中，除第一次归结可用给定子句集的任意字句外，其后的各次归结则至少要有一个亲本子句是上次归结的结果。

线性归结的归结演绎树如图所示：

线性归结的特点是：它本身不仅是完备的且高效的，还能与许多别的策略兼容，例如在线性归结中可同时采用支持集策略或输入策略。

Horn字句

子句的蕴涵表示形式

子句是若干文字的析取，析取词又满足交换律，因此，对于任一个子句，总可以将其表示成如下形式：
$$\neg \mathrm{Q}{1} \mathrm{v} \ldots \mathrm{v} \neg \mathrm{Q}{\mathrm{n}} \mathrm{vP}{1} \mathrm{v} \ldots \mathrm{vP}{\mathrm{m}}$$

可进一步变形为
$$\mathrm{Q}{1} \wedge \mathrm{Q}{2} \wedge \ldots \wedge \mathrm{Q}{\mathrm{n}} \rightarrow \mathrm{P}{1} \vee \mathrm{P}{2} \vee \ldots \vee \mathrm{P}{\mathrm{m}}$$

如果约定蕴含式前件的文字之间恒为合取关系，而蕴含式后件的文字恒为析取关系，那么上述公式可改写为：

$$\mathrm{Q}{1}, \mathrm{Q}{2}, \ldots, \mathrm{Q}{\mathrm{n}} \rightarrow \mathrm{P}{1}, \mathrm{P}{2}, \ldots, \mathrm{P}{\mathrm{m}}$$

一般的，这种蕴含式子句的归结过程可表示如下：

设子句

$$\mathrm{C} : \mathrm{P}{1}, \ldots, \mathrm{P}{\mathrm{m}} \leftarrow \mathrm{Q}{1}, \ldots, \mathrm{Q}{\mathrm{n}}$$

和

$$\mathrm{C}^{\prime} : \mathrm{P}{1}^{\prime}, \ldots, \mathrm{P}{\mathrm{s}}^{\prime} \leftarrow \mathrm{Q}{1}^{\prime}, \ldots, \mathrm{Q}{\mathrm{t}}^{\prime}$$

其中有$P_i$和$Q’_j$可合一，$\sigma$为它们的MGU，则$C$和$C’$的归结式为

$$\mathrm{P}{1} \sigma, \ldots, \mathrm{P}{\mathrm{i}-1} \sigma, \mathrm{P}{\mathrm{i}+1} \sigma, \ldots, \mathrm{P}{\mathrm{m}} \sigma, \mathrm{P}{1}^{\prime} \sigma, \ldots, \mathrm{P}{\mathrm{s}}^{\prime} \sigma \leftarrow \mathrm{Q}{1} \sigma, \ldots, \mathrm{Q}{\mathrm{n}} \sigma, \mathrm{Q}{1}^{\prime} \sigma, \ldots, \mathrm{Q}{\mathrm{j}-1}^{\prime} \sigma, \mathrm{Q}{\mathrm{j}+1}^{\prime} \sigma, \ldots, \mathrm{Q}{\mathrm{t}}^{\prime} \sigma$$

Horn子句消解

定义1 至多含有一个正文字的子句称为Horn子句

由定义，蕴含型Horn子句有下列三种形式：

• $\mathrm{P} \leftarrow \mathrm{Q} 1, \mathrm{Q} 2, \ldots, \mathrm{Q}_{\mathrm{m}}$称为条件子句，P称为头部或结论
• $P \leftarrow $称为无条件句
• $\leftarrow \mathrm{Q}{1}, \mathrm{Q}{2}, \ldots, \mathrm{Q}_{\mathrm{m}}$称为目标子句，$Q_i$称为子目标。

可以看出，Horn子句形式简明，逻辑意义清晰，更重要的是，Horn子句的消解过程可与计算机程序的执行过程统一起来。

SLD Resolution

通过以上讨论，我们就明白了通过Horn子句，运用线性消解策略，实现消解的方法，就是SLD消解。

其中，归结过程实际上是对第一个目标的求解导致了一连串的目标求解，因此目标求解的过程类似于计算机程序执行中的过程调用。

从计算机程序的角度看，条件子句都是”过程“，结论P就是过程名，而P的过程体，即条件子句的后件，可以视为一系列子过程。条件子句的消解可以看做是对结论P的调用，而对P的调用又引起了对子过程的调用，就这样层层调用，直到遇到无条件句，即事实(fact)。

总结

Horn子句是一个至多含有一个正文字的子句，事实( fact )是单位Horn子句的正文字（即无条件句），程序字句是Horn子句的一个正文字和多个负文字（即条件子句），目标子句没有正文字。

逻辑程序( logic program )由一组条件子句和无条件句组成，给定一个逻辑程序和目标子句，SLD消解能被用于搜索互斥（以便于反证）。如果驳斥存在，那么目标子句的取反就是条件子句和无条件句的结果，然后在驳斥过程中的替换就是逻辑程序的答案。[5]

Reference

[1] Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973. Also in Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574.

[2] Robert Kowalski and Donald Kuehner, Linear Resolution with Selection Function Artificial Intelligence, Vol. 2, 1971, pp. 227-60.

[3] J.W. Lloyd. Mathematical Logic for Computer Science (Third Edition). Springer, London, 2012, pp. 205

[4] Schmerl, U.R. Resolution on Formula-Trees. Acta Informatica. 1988, 25: 425–438. doi:10.1007/bf02737109. Summary

[5] J.W. Lloyd. Mathematical Logic for Computer Science (Third Edition). Springer, London, 2012, pp. 220