消解序列

定义 设 $S$ 是一个合取范式, $C_1,...,C_n$ 是一个简单析取式序列, 如果对每一个 $i$, $C_i$ 是 $S$ 的一个简单析取式或是 $Res(C_j,C_k)$, 则称此序列是由 $S$ 导出 $C_n$ 的消解序列.

当 $C_n=\lambda$ 时, 称此序列是 $S$ 的一个否证.