在命题逻辑中的归结规则是一个单一的有效的
推理规则,从两个
子句生成它们所蕴含的一个新的子句。归结规则接受包含互补的文字的两个子句 - 子句是
文字的析取式,并生成带有除了互补的文字的所有文字的一个新子句。形式上,这里的和是互补的文字:
当两个子句包含多于一对的互补文字的时候,归结规则可以(独立的)应用到每个这种文字对上。但是,只有要消去(resolve)的文字对可以去除:所有其他文字对仍保留在归结后的子句中。
当外加上完备的
查找算法的时候,归结规则生成一个可靠的和完备的算法来决定命题公式的可满足性,并且经过扩展,决定句子在一组公理下的有效性。
这个算法的一个实例是最初的Davis-Putnam算法,它后来被精制成去除了对归结出的子句的显式表示的需求的
DPLL算法。