归结（resolution）原理，在数理逻辑和自动定理证明中（GOFAI涉及的主题），是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。
在命题逻辑中的归结规则是一个单一的有效的推理规则，从两个子句生成它们所蕴含的一个新的子句。归结规则接受包含互补的文字的两个子句 - 子句是文字的析取式，并生成带有除了互补的文字的所有文字的一个新子句。形式上，这里的（resolvent）。
当两个子句包含多于一对的互补文字的时候，归结规则可以（独立的）应用到每个这种文字对上。但是，只有要消去（resolve）的文字对可以去除：所有其他文字对仍保留在归结后的子句中。
当外加上完备的搜索算法的时候，归结规则生成一个可靠的和完备的算法来决定命题公式的，并且经过扩展，决定句子在一组公理下的有效性。
这种归结技术使用反证法，并基于在命题逻辑中的任何句子都能转换成等价的合取范式句子的事实。步骤如下：
这个算法的一个实例是最初的Davis-Putnam算法，它后来被精制成去除了对归结出的子句的显式表示的需求的DPLL算法。
一阶逻辑归结把传统的逻辑推理的直言三段论浓缩成了一个单一的规则。
要理解归结是如何工作的，考虑词项逻辑三段论的下列例子：
或者，更一般性的：
要使用归结技术重造推理，首先子句们必须转换成合取范式。在这种形式下，所有的量化都成为隐含的：在变量（X, Y...）上的全称量词理所当然的被省略了，而存在量化的变量被替换成Skolem函数。
所以，问题是归结技术如何从前两个子句推导出最后一个子句?规则是简单的：
要应用这个规则到上述例子，我们找到谓词P以否定形式出现在第一个子句中
并以非否定形式出现在第二个子句中
X是一个未绑定变量，而a是一个绑定变量（原子）。合一两个子句生成代换（substitution）
丢弃合一了的谓词，并把这个代换应用到余下的谓词中（在本例中就是Q（X）)，生成结论：
举个其他例子，考虑三段论形式
或者更一般性的,
在合取范式中，前提变成了：
（注意在第二个子句中的变量被重命名来使在不同子句中的变量清晰的区分开来。）
现在，合一第一个子句中的Q（X）和第二个子句中¬Q（Y）意味着X和Y变成了同一个变量。把这个变量代换到余下的子句中，合并它们给出结论：
归结规则（带有额外的因数分解）同样的包容传统逻辑的所有其他的演绎形式。
Paramodulation是一种相关技术，用于推理条款集，其中谓词变量是平等的。它可以生成所有 "相等 "的子句，但反身的相同性除外。参数化操作需要一个正的子句，它必须包含一个平等字面。然后，它搜索一个 "进入 "子句，该子句与平等关系的一方相统一。然后，该子项被等号的另一边所取代。Paramodulation的一般目的是将系统简化为原子，在替换时减少术语的大小。
Approaches to non-clausal resolution, i.e. resolution of first-order formulas that need not be in clausal normal form, are presented in:
