導出原理
プラウィツ(Dag Prawitz)は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入(単一化)によって充足不能性を調べる方法を1960年に提案した。 この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形は全ての連言項を調べなければならないため全体の効率はいいとは言えなかった。
ロビンソンはデービス・パトナムの枠組みにプラウィツのアイデアを組み合わせ、ただ1つの導出規則と単一化による代入操作とで充足不能性を調べる導出原理を1965年に発表した。単純な規則で関係する論理式のみを段階的に具体化していく方法は、従来の方法よりはるかに効率がよく、また理論的なエレガントさを持っていたため、その後の定理自動証明に大きな影響を与えた。
さらに3番目は以下の節になる。
C 4 = ¬ R ( a ) {\displaystyle C_{4}=\lnot R(a)}
証明したい論理式の否定は以下の節である。
C 5 = ¬ P ( a ) {\displaystyle C_{5}=\lnot P(a)}
これらの節 C 1 , C 2 , C 3 , C 4 , C 5 {\displaystyle {C_{1},C_{2},C_{3},C_{4},C_{5}}} が反駁の対象となる節集合である。
C 3 {\displaystyle C_{3}} と C 4 {\displaystyle C_{4}} の R {\displaystyle R} についての導出を考えると、 { x / a } {\displaystyle \left\{x/a\right\}} の代入により以下が導かれる。
C 6 = S ( a ) {\displaystyle C_{6}=S\left(a\right)}
C 1 {\displaystyle C_{1}} と C 6 {\displaystyle C_{6}} の S {\displaystyle S} についての導出を考えると、
C 7 = P ( a ) {\displaystyle C_{7}=P\left(a\right)}
最後に C 5 {\displaystyle C_{5}} と C 7 {\displaystyle C_{7}} の導出により空節 □ が導かれ、 P ( a ) {\displaystyle P\left(a\right)} が成り立つことを証明できる。