導出原理
p → q {\displaystyle p\to q} を節形式にすると ¬ p ∨ q {\displaystyle \lnot p\lor q} となる。 C R {\displaystyle C_{R}} を C 1 , C 2 {\displaystyle C_{1},C_{2}} の導出節とすると、前件肯定は以下の導出と同じである。
C 1 = ¬ p ∨ q ( p → q ) C 2 = p C R = q ( r e s o l v e n t ) {\displaystyle {\begin{array}{ll}C_{1}=\lnot p\lor q&\left(p\to q\right)\\C_{2}=p\\C_{R}=q&\left(\mathrm {resolvent} \right)\end{array}}}
以下の節からの導出を考える。
C 1 = ¬ P ( x ) ∨ ¬ Q ( y ) ∨ R ( x , y ) {\displaystyle C_{1}=\lnot P(x)\lor \lnot Q(y)\lor R(x,y)}
C 2 = Q ( a ) {\displaystyle C_{2}=Q\left(a\right)}
C 3 = P ( b ) {\displaystyle C_{3}=P\left(b\right)}
Q を単一化する代入 { y / a } {\displaystyle \left\{y/a\right\}} により C 1 {\displaystyle C_{1}} と C 2 {\displaystyle C_{2}} の導出を行うと、
C R = ¬ P ( x ) ∨ R ( x , a ) {\displaystyle C_{R}=\lnot P(x)\lor R(x,a)}
続いて、P を単一化する代入 { x / b } {\displaystyle \left\{x/b\right\}} により C R {\displaystyle C_{R}} と C 3 {\displaystyle C_{3}} の導出を行うと、
C S = R ( b , a ) {\displaystyle C_{S}=R\left(b,a\right)}
を得ることができる。