導出原理（どうしゅつげんり、英: resolution principle）とは、ジョン・アラン・ロビンソン
（英語版）により1965年に提案された[1]原理または手法を言う。導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。 述語論理式 P が恒真であるかを証明する一般的な手続きは存在しないが、1930年に発表されたエルブランの定理はエルブラン領域の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、¬P が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には単一化アルゴリズムなど他の様々なものが含まれていた[2]。 1950年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960) が考案された。デービス・パトナムのアルゴリズムには連言標準形の使用や導出規則の考え方が含まれていた。しかし、これらはエルブランの定理の証明を直接計算機上で実現したような方法で、エルブラン領域の要素を順次生成して変数を含まない論理式(基礎例)を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった[3]。 プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入（単一化）によって充足不能性を調べる方法を1960年に提案した[4]。この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形は全ての連言項を調べなければならないため全体の効率はいいとは言えなかった。 ロビンソンはデービス・パトナムの枠組みにプラウィツのアイデアを組み合わせ、ただ1つの導出規則と単一化による代入操作とで充足不能性を調べる導出原理を1965年に発表した。単純な規則で関係する論理式のみを段階的に具体化していく方法は、従来の方法よりはるかに効率がよく、また理論的なエレガントさを持っていたため、その後の定理自動証明に大きな影響を与えた[3]。 導出とは二つの節より新しい節を導き出す操作で、一方の節に含まれるリテラル l {\displaystyle l} と、他方の節に含まれる否定リテラル ¬ l {\displaystyle \neg l} をのぞき、その他のリテラルの論理和をとることで、新しい節を得ることをいう。 命題論理での導出規則を式で表せば、 l ∨ P , ¬ l ∨ Q P ∨ Q {\displaystyle {\frac {l\vee P,\quad \neg l\vee Q}{P\vee Q}}} と書ける。ここで上式は前提となる親節、下式はそれらから導かれる導出節（resolvent）を表す。 あるいは、別の表記法を用いて次のようにも表現できる。前提となる節を C 1 {\displaystyle C_{1}} と C 2 {\displaystyle C_{2}} とし, もしリテラル L ∈ C 1 {\displaystyle L\in C_{1}} と否定リテラル L ¯ ∈ C 2 {\displaystyle {\overline {L}}\in C_{2}} が存在するならば、導出節 C R {\displaystyle C_{R}} は以下のようになる。 C R = ( C 1 ∖ { L } ) ∪ ( C 2 ∖ { L ¯ } ) {\displaystyle C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})}
目次
1 背景
2 定義
2.1 例
3 一階述語論理での導出
3.1 例
4 反駁による証明
4.1 例
5 証明戦略
6 脚注
7 関連項目
8 参考文献
9 外部リンク
背景
定義