归结法

关于命题逻辑的语义学的一课表明，有效性和可满足性可以用真值表判定，其代价随每个变元翻一番，并预告了无须遍历真值表的方法。关于语义后承与语义等价的一课把每个后承归结为一个不可满足性：$\Gamma \models \varphi$ 当且仅当 $\Gamma \cup \{\neg\varphi\}$ 不可满足。关于范式以及关于范式算法的两课给每个公式一个合取形式，其有效性一眼可见，但其可满足性却看不出来。若是如此，就还缺少一个直接作用于子句本身、判定子句合取之不可满足性的程序。这个程序就是归结，由约翰·艾伦·鲁宾逊于 1965 年在马丁·戴维斯和希拉里·普特南（1960）思想的基础上提出；它是今天判定含有数百万变元之公式的可满足性的程序的核心。演绎单元的系统与语义学的关系由关于可靠性与完备性以及关于紧致性定理的两课研究；与该系统不同，归结并不推演出结论：它反驳集合。本课证明它这样做是可靠且完备的。

与前面各课一样，$p$、$q$、$r$、$s$ 和 $t$ 表示变元 $v_1$ 至 $v_5$；不带下标的字母 $v$ 以及 $w$ 表示赋值；$V(\varphi)$ 是 $\varphi$ 的变元集合。

子句与子句集合

回忆关于范式的一课：文字是一个变元或一个变元的否定；一个文字 $\ell$ 的相反文字记作 $\ell^{*}$，是同一变元、符号相反的文字；两个相反的文字构成一个互补对。由文字的否定引理，$v(\ell^{*}) = 1 - v(\ell)$ 对每个赋值 $v$ 都成立。在那里子句是文字的析取；在这里宜于忘掉次序和重复（它们不改变值），只保留集合。

子句是文字的有穷集合。没有文字的子句称为空子句，记作 $\Box$。赋值 $v$ 满足子句 $C$，记作 $v \models C$，是指 $C$ 中某个文字取值 $1$（在 $v$ 中）；否则，$v$ 反驳它。只有一个文字的子句称为单元子句。一个子句的变元构成集合 $V(C)$；一个子句集合 $S$ 的变元构成集合 $V(S)$，即前者的并。一个赋值满足子句集合 $S$，记作 $v \models S$，是指它满足其中的每个子句；若某个赋值满足 $S$，则称它是可满足的，否则称它是不可满足的。最后，若 $S$ 是子句集合而 $C$ 是子句，$S \models C$ 表示每个满足 $S$ 的赋值都满足 $C$。

由定义得出两种极端情形，宜于确定下来。空子句没有文字；因此，它没有文字取值 $1$，也没有赋值满足它：$\Box$ 不可满足，包含它的每个集合也不可满足。反之，空的子句集合没有需要满足的子句，每个赋值都满足它。二者不可混淆：$\{\Box\}$ 不可满足，而 $\emptyset$ 被所有赋值满足。

含有互补对的子句称为重言子句：它不施加任何条件，可以从任何集合中去掉而不改变其模型。把子句写成集合并非记号上的任性。若要由 $(p \vee q)$ 和 $(p \vee \neg q)$ 得到 $p$，析取给出 $(p \vee p)$，它等价于 $p$，却不是同一个公式；用集合则有 $\{p\} \cup \{p\} = \{p\}$，重复文字的合并自动发生。