導出原理

健全性。 付値 $v$ が $C_1\ni\ell$ と $C_2\ni\overline\ell$ を満たすとする。$v(\ell)$ が真なら $\overline\ell$ は偽なので $C_2\setminus\{\overline\ell\}$ のあるリテラルが真であり、偽なら $C_1\setminus\{\ell\}$ のあるリテラルが真である。どちらでも導出節は $v$ で満たされる。よって $S$ を満たす付値は導出のすべての節を満たし、$\square$ は満たさないので、反駁があれば $S$ は充足可能でない。
完全性。 $S$ に現れる命題変数の個数 $n$ に関する帰納法で示す。$n=0$ なら $S$ の元は $\square$ だけで、$S$ が充足可能でないなら $S\ne\emptyset$ なので $\square\in S$ であり、1 行の列 $\square$ が反駁である。$n\ge1$ として、$S$ に現れる命題変数 $P$ を 1 つとり、
$$ S^{+}:=\{C\setminus\{\lnot P\}\mid C\in S,\ P\notin C\},\qquad S^{-}:=\{C\setminus\{P\}\mid C\in S,\ \lnot P\notin C\} $$
とおく（$P$ を真、偽と決めたときに残る条件である）。どちらにも $P$ は現れない。
$S^{+}$ は充足可能でない。実際、$S^{+}$ を満たす付値 $v$ を $P$ で真に変えた付値 $v'$ は、$P\in C$ となる $C$ を満たし、$P\notin C$ となる $C$ も満たす（$C\setminus\{\lnot P\}$ を満たすリテラルは $P$ を含まないので $v'$ でも真）。これは $S$ が充足可能でないことに反する。同じく $S^{-}$ も充足可能でない。帰納法の仮定により $S^{+}$ と $S^{-}$ の反駁がある。
次の主張を示す：$S^{+}$ からの導出 $D_1,\dots,D_k$ に対し、$S$ からの導出 $D_1',\dots,D_k'$ で $D_j'\in\{D_j,\ D_j\cup\{\lnot P\}\}$ となるものがある。$D_j\in S^{+}$ なら $D_j=C\setminus\{\lnot P\}$（$C\in S$）なので $D_j':=C$ とする。$D_j$ が $D_i,D_{i'}$ の $\ell$ についての導出節なら、$\ell$ は $P$ でも $\lnot P$ でもない（$S^{+}$ からの導出に $P$ は現れない）ので、$\ell\in D_i'$、$\overline\ell\in D_{i'}'$ であり、$D_j':=(D_i'\setminus\{\ell\})\cup(D_{i'}'\setminus\{\overline\ell\})$ は $D_j$ か $D_j\cup\{\lnot P\}$ である。
$S^{+}$ の反駁にこれを使うと、$S$ から $\square$ か $\{\lnot P\}$ が導出できる。同様に $S^{-}$ の反駁から、$S$ から $\square$ か $\{P\}$ が導出できる。どちらかで $\square$ が出れば終わりで、そうでなければ 2 つの導出をつなぎ、$\{P\}$ と $\{\lnot P\}$ の導出節 $\square$ を最後に加えればよい。$\square$

要点：$E$ のどの単一化子 $\theta$ についても $\sigma_k\theta=\theta$ が保たれる。各段で変数が 1 つ消えるので算法は止まり、止まったときの $\sigma_k$ が最汎単一化子になる。

def-resolution-first-order の記号で、$\sigma$ を $E$ の最汎単一化子、$E\sigma=\{A_0\}$ とする。割り当て $s$ を任意にとり、$s'(x):=(x\sigma)^{\mathcal M}[s]$ とおく。項の組み立てに沿った帰納法で $(t\sigma)^{\mathcal M}[s]=t^{\mathcal M}[s']$ であり、したがってリテラル $\ell$ について $\mathcal M\models\ell\sigma[s]\iff\mathcal M\models\ell[s']$ である。$\mathcal M\models\forall C_1$ なので、$C_1$ のあるリテラル $\ell_1$ で $\mathcal M\models\ell_1[s']$、すなわち $\mathcal M\models\ell_1\sigma[s]$ となる。同様に $C_2$ のあるリテラル $\ell_2$ で $\mathcal M\models\ell_2\sigma[s]$ となる。$\ell_1\in L_1$ かつ $\ell_2\in M_2$ なら $\ell_1\sigma=A_0$、$\ell_2\sigma=\lnot A_0$ がともに $s$ のもとで真となり不可能である。よってどちらかは $C_1\setminus L_1$ か $C_2\setminus M_2$ に属し、その $\sigma$ による像は $R$ のリテラルで $s$ のもとで真である。$s$ は任意なので $\mathcal M\models\forall R$。$\square$

$D$ を基礎原子論理式 $A$ についての導出節とし、$A\in C_1\theta$、$\lnot A\in C_2\theta$ とする（逆の場合は $C_1$ と $C_2$ を入れ替える）。
$$ L_1:=\{\ell\in C_1\mid\ell\theta=A\},\qquad M_2:=\{\ell\in C_2\mid\ell\theta=\lnot A\} $$
とおく。どちらも空でなく、$L_1$ は原子論理式、$M_2$ は否定だけからなる。$\theta$ は $E=L_1\cup\{B\mid\lnot B\in M_2\}$ を $\{A\}$ に写すので単一化子であり、thm-resolution-unification により最汎単一化子 $\sigma$ と $\lambda$ で $\theta=\sigma\lambda$ となるものがある。$R:=((C_1\setminus L_1)\cup(C_2\setminus M_2))\sigma$ は $C_1,C_2$ の導出節で、
$$ R\lambda=(C_1\setminus L_1)\theta\cup(C_2\setminus M_2)\theta . $$
$C_1\setminus L_1$ の元は $\theta$ で $A$ 以外に写り、$C_1\theta\setminus\{A\}$ の元は $L_1$ に属さない $C_1$ の元の像なので、$(C_1\setminus L_1)\theta=C_1\theta\setminus\{A\}$ である。同様に $(C_2\setminus M_2)\theta=C_2\theta\setminus\{\lnot A\}$ であり、$R\lambda=D$ である。$\square$

反駁があれば充足可能でないことは上で示した。逆に $S$ が充足可能でないとする。$\square\in S$ なら 1 行の列 $\square$ が反駁なので、$\square\notin S$ とする（このとき下の $\bigvee C$ はどれも論理式である）。$S$ に現れる記号の言語に、定数記号がなければ 1 つ加えた言語を $L$ とする（加えた記号を自由に解釈すればよいので、充足可能性は変わらない）。$S$ の節に現れる変数を $\bar x=(x_1,\dots,x_n)$ とし、量化記号のない論理式 $\psi:=\bigwedge_{C\in S}\bigvee C$ をとる。$\forall$ は $\land$ に分配するので、$S$ が充足可能でないことは文 $\forall\bar x\,\psi$ が充足可能でないことと同じである。Herbrandの定理 の系「全称文についての Herbrand の定理」により、閉項の組 $\bar t_1,\dots,\bar t_m$ で $\psi(\bar t_1)\land\cdots\land\psi(\bar t_m)$ が命題論理の意味で充足可能でないものがある。$\theta_j:=\{x_i\mapsto t_{j,i}\}_i$ とおくと、これは基礎節の有限集合 $G:=\{C\theta_j\mid C\in S,\ 1\le j\le m\}$ が充足可能でないことにあたる。thm-resolution-propositional により $G$ の反駁 $D_1,\dots,D_k=\square$ がある。
各 $j$ について、$S$ からの導出で得られる節 $F_j$ と代入 $\lambda_j$ で $F_j\lambda_j=D_j$ となるものがあることを、$j$ に関する帰納法で示す。$D_j\in G$ なら $D_j=C\theta_{j'}$ なので $F_j:=C$ とする。$D_j$ が $D_i,D_{i'}$ の導出節なら、$F_{i'}$ の変種 $F'$ で $F_i$ と共通の変数をもたないものをとり、名前の付け替えを戻してから $\lambda_{i'}$ を施す代入を $\lambda'$ とすると $F'\lambda'=D_{i'}$ である。$F_i$ の変数では $\lambda_i$、$F'$ の変数では $\lambda'$ と一致する代入 $\theta$ をとると $F_i\theta=D_i$、$F'\theta=D_{i'}$ であり、lem-resolution-lifting により $F_i,F'$ の導出節 $F_j$ と $\lambda_j$ で $F_j\lambda_j=D_j$ となるものがある。$F_j$ は $S$ からの導出の次の行になる。
最後に $F_k\lambda_k=\square$ なので $F_k=\square$ であり、$S$ の反駁が得られた。$\square$