在两个子句间消去一对文字
归结处理子句，即文字的析取；文字可以是命题字母或其否定，一阶逻辑中则可以含谓词和项。命题归结的基本形式是：由p∨A和¬p∨B推出A∨B，其中A、B代表其余文字。只要两个前提都真，所得子句就不可能为假，所以这是可靠的推理规则。
例如，由p∨q及¬p∨r可推出q∨r。它不是把所有看起来相反的文字同时删除：p∨q与¬p∨¬q只能在选定的一对互补文字上归结，在p上归结得到q∨¬q，而不是空子句。前两句实际上可以同时成立，误删两对文字会凭空制造矛盾。
参考：[1]
把证明转成寻找矛盾
要证明前提集蕴含目标Q，可把¬Q加入前提，将公式转为合适的子句形式，再持续归结。若得到没有任何文字的空子句，就说明扩充后的前提不可同时满足，从而原前提蕴含Q。空子句表示假，不能与“没有任何子句约束”的空子句集混为一谈。
以P和¬P∨Q为前提，加入¬Q后，后两句归结得到¬P，再与P归结得到空子句。因此Q得到证明。归结产生的中间子句应保留其父子句和所用替换，才能检查证明的每一步，而非只依赖程序声称成功。
一阶归结中的合一
一阶逻辑允许变量和函数项，互补文字可能在替换后才匹配。例如P(x)与¬P(a)∨R(a)可用x替换为a进行归结，推出R(a)。若变量还出现在同一父子句的其他位置，替换必须一致地作用于整个父子句，不能只修改被删除的那一个文字。
不同子句中的变量先按需要改成互不混淆的名字；合一则寻找使相应原子式一致的替换。标准有限项合一还要检查变量是否出现在拟替换它的项中，例如不能把x简单替换成f(x)。这些步骤使一阶归结不同于单纯的字符串删除。
完备性所保证的范围
归结反证的关键性质是反驳完备性：在适用的演算及完整搜索条件下，不可满足的子句集能够被归结反驳。它不表示裸的二元归结会直接列出所有逻辑后果；例如单独的P蕴含P∨R，但没有第二个互补父子句供这条规则直接产生后者。
控制策略决定先处理哪些子句。只允许某些推理可能提高速度，却也可能损失完备性；“优先使用单元子句”与“只能使用单元子句”并不相同。尤其在一般一阶逻辑中，目标并非前提后果时，归结搜索可能不终止，不能把迟迟没有找到矛盾当成已经证明可满足。