導出原理（どうしゅつげんり、）とは、により1965年に提案された原理または手法を言う。導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。述語論理式 "P" が恒真であるかを証明する一般的な手続きは存在しないが、1930年に発表されたエルブランの定理はエルブラン領域の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、"¬P" が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には単一化アルゴリズムなど他の様々なものが含まれていた。1950年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960) が考案された。デービス・パトナムのアルゴリズムには連言標準形の使用や導出規則の考え方が含まれていた。しかし、これらはエルブランの定理の証明を直接計算機上で実現したような方法で、エルブラン領域の要素を順次生成して変数を含まない論理式("基礎例")を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった。プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入（単一化）によって充足不能性を調べる方法を1960年に提案した。この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形は全ての連言項を調べなければならないため全体の効率はいいとは言えなかった。ロビンソンはデービス・パトナムの枠組みにプラウィツのアイデアを組み合わせ、ただ1つの導出規則と単一化による代入操作とで充足不能性を調べる導出原理を1965年に発表した。単純な規則で関係する論理式のみを段階的に具体化していく方法は、従来の方法よりはるかに効率がよく、また理論的なエレガントさを持っていたため、その後の定理自動証明に大きな影響を与えた。"導出"とは二つの節より新しい節を導き出す操作で、一方の節に含まれるリテラル formula_1 と、他方の節に含まれる否定リテラル formula_2 をのぞき、その他のリテラルの論理和をとることで、新しい節を得ることをいう。命題論理での導出規則を式で表せば、formula_3と書ける。ここで上式は前提となる"親節"、下式はそれらから導かれる"導出節"（）を表す。あるいは、別の表記法を用いて次のようにも表現できる。前提となる節を formula_4 と formula_5 とし, もしリテラル formula_6 と否定リテラル formula_7 が存在するならば、導出節 formula_8 は以下のようになる。導出規則は三段論法や前件肯定を一般化した規則となっている。導出は完全な証明系であることが知られている。formula_10 を節形式にすると formula_11 となる。formula_12 をformula_13 の導出節とすると、前件肯定は以下の導出と同じである。同様に、formula_10、formula_16 の節形式 formula_17、 formula_18 による三段論法は以下のようになる。述語論理のリテラルには個体変数が含まれるため、リテラルと否定リテラルとを単純に比較するだけでは削除できるかどうか分からない。一階述語論理ではリテラルと否定リテラルそれぞれの原子論理式が単一化できる場合に導出を行う。また、導出の対象となる節は、冠頭標準形にして存在記号を削除したスコーレム連言標準形の論理式である。例えば、一方の節がリテラル formula_20、もう一方の節がリテラル formula_21 を含む場合、適切な代入 formula_22 により各リテラルは formula_23、 formula_24 と書き換えられ、同じにすることができる。ここで代入 formula_25 は formula_26、formula_27 に書き換えることを表す。一般に論理式 formula_28 を等しくする代入を formula_28 の"単一化子"（）といい、そのうち最も一般的な単一化子（"最汎単一化子"）を formula_28 の"mgu"（）という。上記の例の場合、両方の論理式を等しくする代入は formula_31、formula_32 など無数に存在する。これらは本来の代入 formula_25 に formula_34 などの代入を合成したものなので、最汎単一化子 mgu は formula_25 である。一階述語論理での導出は mgu を用いて次のように表現できる。もしリテラル formula_36 と否定リテラル formula_37 が存在し、 formula_38 と formula_39 が mgu formula_40 を持つ場合、以下の formula_8 が"2項導出節"（）である。ここで、formula_42 などは、それぞれの節やリテラルに代入 formula_40 を行ったものを表す。同様のやり方での2以上の複数の節から同時に導出することも可能であり、"超導出"（）と呼ばれる。以下の節からの導出を考える。"Q" を単一化する代入 formula_48 により formula_49 と formula_50の導出を行うと、続いて、"P" を単一化する代入 formula_52 により formula_12 と formula_54の導出を行うと、を得ることができる。反駁（はんばく、）とは、節の集合からの導出により空節 □ を導くことである。反駁については以下の定理が成り立つ。節の集合 "S" が充足不能である必要十分条件は、節の集合 "S" からの導出により空節 □ が導けることである。これはエルブランの定理を導出に応用したものになっている。論理式 "P" が恒真であれば formula_56 は充足不能（恒偽）であるため、節の集合に formula_56 を追加し導出を繰り返すことで空節 □ になれば、論理式 "P" が恒真であることが証明できる。反駁により formula_58 が formula_59 の論理的帰結か調べるアルゴリズムは以下のように表現できる。以下の公式が成り立つ時、formula_77 が成り立つかどうかを証明する場合を考える。反駁の対象となる論理式は以下の論理式に formula_78 を追加したものである。最初の論理式は formula_82 と等価なため、次の2つの節で表現できる。2番目の論理式は以下の節になる。 さらに3番目は以下の節になる。証明したい論理式の否定は以下の節である。これらの節 formula_88 が反駁の対象となる節集合である。formula_89 と formula_90 の formula_91 についての導出を考えると、formula_34 の代入により以下が導かれる。formula_4 と formula_95 の formula_96 についての導出を考えると、最後に formula_98 と formula_99 の導出により空節 □ が導かれ、formula_77 が成り立つことを証明できる。導出は２つの節を前提として導出節を導くものであるので、どの節に導出規則を適用するかについては様々な選択肢があり、そのやり方により効率が大幅に異なる。代表的な証明戦略として以下のものがある。

出典:wikipedia