導出原理
一階述語論理での導出は mgu を用いて次のように表現できる。
もしリテラル L 1 ∈ C 1 {\displaystyle L_{1}\in C_{1}} と否定リテラル L 2 ̄ ∈ C 2 {\displaystyle {\overline {L_{2}}}\in C_{2}} が存在し、 L 1 {\displaystyle L_{1}} と L 2 {\displaystyle L_{2}} が mgu σ {\displaystyle \sigma } を持つ場合、以下の C R {\displaystyle C_{R}} が2項導出節(binary resolvent)である。ここで、 C 1 σ , C 2 σ {\displaystyle C_{1}\sigma ,C_{2}\sigma } などは、それぞれの節やリテラルに代入 σ {\displaystyle \sigma } を行ったものを表す。
C R = ( C 1 σ ∖ { L 1 σ } ) ∪ ( C 2 σ ∖ { L 2 σ ̄ } ) {\displaystyle C_{R}=(C_{1}\sigma \setminus \{L_{1}\sigma \})\cup (C_{2}\sigma \setminus \{{\overline {L_{2}\sigma }}\})}
同様のやり方での2以上の複数の節から同時に導出することも可能であり、超導出(hyper-resolution)と呼ばれる。