归结原理

归结原理是由 Robinson (1965) 提出的，是一种定理证明方法，它通过构造反驳证明，即反证法来进行证明。这种方法已在许多自动定理证明器中得到应用。归结原理适用于 一阶逻辑 中 Skolem 范式 的公式。这些公式基本上是 子句 的集合，其中每个子句是 文字 的 析取。合一 是归结证明中的一项关键技术。

如果子句 中两个或多个正文字（或两个或多个负文字）是可合一的，且 是它们的最一般合一子，那么 被称为 的因子。例如， 被分解为 。在这种因子分解中，重复项被移除。

设 和 是两个没有公共变量的子句，设 包含一个正文字 ， 包含一个负文字 ，且设 是 和 的最一般合一子。那么

被称为 和 的二元归结式。例如，如果 且 ，那么 是它们的二元归结式。

两个子句 和 的归结式是以下四种二元归结式之一。

1. 和 的二元归结式。

2. 和 的因子的二元归结式。

3. 的因子和 的二元归结式。

4. 的因子和 的因子的二元归结式。

从两个子句生成归结式，称为归结，是归结原理的唯一推理规则。归结原理是完备的，因此，一个子句集合（合取）是 不可满足的 当且仅当 可以通过归结从它推导出 空子句。

归结原理完备性的证明基于 Herbrand 定理。由于不可满足性与有效性是对偶的，因此归结原理应用于定理的否定。

已经开发出多种策略来提高归结原理的效率。这些策略有助于选择子句对以应用归结规则。例如，线性归结是以下演绎策略。设 为子句的初始集合。如果 ，则从 线性演绎出 ，其中 顶子句 为 ，是指一种演绎，其中每个 是 和 () 的归结式，并且每个 要么在 中，要么是一个归结式 （其中 ）。

线性归结是完备的，因此，如果 是不可满足的子句集 中的一个子句，并且 是可满足的，那么可以通过以 作为 顶子句 的线性归结获得 空子句。

如果附加限制 必须在 中，那么这种受限策略是不完备的。但是，对于包含 恰好一个 目标的 Horn 子句 集合，并且目标被选为 顶子句，它是完备的。此类集合中的所有其他子句都是确定的 Horn 子句。编程语言 Prolog 的实现就是在这种策略的框架内进行搜索。