「導出原理」の版間の差分

削除された内容追加された内容

インライン

2010年4月5日 (月) 05:04時点における版

導出（どうしゅつ、英: resolution）とは、数理論理学における一つの演繹方法で、三段論法を一般化した導出規則と呼ばれるただ１つの推論規則を用いる。命題論理、述語論理のいずれにも使う事ができ、導出を繰り返すことで証明したい論理式の否定から空節が導かれることにより証明を行う。導出規則と単一化にもとづく導出原理（どうしゅつげんり、英: resolution principle）はジョン・アラン・ロビンソン（英語版）により1965年に提案され^[1]、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。

背景

述語論理式 P が恒真であるかを証明する一般的な手続きは存在しないが、1930年に発表されたエルブランの定理はエルブラン領域の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、 $\lnot P$ が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には単一化アルゴリズムなど他のさまざまなものが含まれていた^[2]。

1950年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)やデービス・パットナムのアルゴリズム(1958,1960) が考案された。これらはエルブランの定理の証明を直接計算機上で実現したような方法で、エルブラン領域の要素を順次生成して変数を含まない論理式(基礎例)を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった^[3]。

プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入（単一化）によって充足不能性を調べる方法を1960年に提案した^[4]。この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形はすべての連言項を調べなければならないため全体の効率はいいとは言えなかった。

ロビンソンはデービス・パットナムの枠組みにプラウィツのアイデアを組み合わせ、ただ１つの導出規則と単一化による代入操作とで充足不能性を調べる導出原理を1965年に発表した。単純な規則で関係する論理式のみを段階的に具体化していく方法は、従来の方法よりはるかに効率がよく、また理論的なエレガントさを持っていたためで、その後の定理自動証明に大きな影響を与えた^[3]。

定義

導出とは二つの節より新しい節を導きだす操作で、一方の節に含まれるリテラル $l$ と、他方の節に含まれる否定リテラル $\neg l$ をのぞき、その他のリテラルの論理和をとることで、新しい節を得ることをいう。

命題論理での導出規則を式で表せば、 ${\frac {l\vee P,\quad \neg l\vee Q}{P\vee Q}}$ と書ける。ここで上式は前提となる節、下式はそれらから導かれる導出節（resolvent）を表わす。

あるいは、別の表記法を用いれば、前提となる節を $C_{1}$ と $C_{2}$ とし, もしリテラル $L\in C_{1}$ と否定リテラル ${\overline {L}}\in C_{2}$ が存在すれば、導出節 $C_{R}$ は以下のようになる。

C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})

これは三段論法や前件肯定を一般化した規則となっている。導出は完全な証明系であることが知られている。

例

$p\to q$ を節形式にすると $\lnot p\lor q$ となる。 $C_{R}$ を $C_{1},C_{2}$ の導出節とすると、前件肯定は以下の導出と同じである。

{\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}}

同様に、 $p\to q$ 、 $q\to r$ の節形式 $\lnot p\lor q$ 、 $\lnot q\lor r$ による三段論法は以下のようになる。

{\begin{array}{ll}C_{1}=\lnot p\lor q&\left(p\to q\right)\\C_{2}=\lnot q\lor r&\left(q\to r\right)\\C_{R}=\lnot p\lor r&\left(\mathrm {resolvent,\ } p\to r\right)\end{array}}

一階述語論理での導出

述語論理のリテラルには個体変数が含まれるため、リテラルと否定リテラルとを単純に比較するだけでは削除できるかどうか分からない。一階述語論理ではリテラルと否定リテラルそれぞれの原子論理式が単一化できる場合に導出を行う。

また、導出の対象となる節は、冠頭標準形にして存在記号を削除したスコーレム連言標準形の論理式である。

例えば、一方の節がリテラル $p(x,y)$ 、もう一方の節がリテラル $\lnot p(z,f(b))$ を含む場合、適切な代入 $\sigma =\left\{z/x,y/f(b)\right\}$ により各リテラルは $p(x,f(b))$ 、 $\lnot p(x,f(b))$ と書き換えられ、同じにすることができる。ここで代入 $\left\{z/x,y/f(b)\right\}$ は $z\to x$ 、 $y\to f(b)$ に書き換えることを表わす。

一般に論理式 $F_{1},F_{2}$ を等しくする代入を $F_{1},F_{2}$ の単一化子（unifier）といい、そのうち最も一般的な単一化子（最汎単一化子）を $F_{1},F_{2}$ のmgu（most general unifier）という。上記の例の場合、両方の論理式を等しくする代入は $\left\{z/a,y/f(b),x/a\right\}$ 、 $\left\{z/x,y/c,f(b)/c\right\}$ など無数に存在する。これらは本来の代入 $\left\{z/x,y/f(b)\right\}$ に $\left\{x/a\right\}$ などの代入を合成したものなので、最汎単一化子 mgu は $\left\{z/x,y/f(b)\right\}$ である。

一階述語論理での導出は次のように表現できる。もしリテラル $L_{1}\in C_{1}$ と否定リテラル ${\overline {L_{2}}}\in C_{2}$ が存在し、 $L_{1}$ と $L_{2}$ が mgu $\sigma$ を持つ場合、以下の $C_{R}$ を節 $C_{1}$ と $C_{2}$ との２項導出節という。

C_{R}=(C_{1}\sigma \setminus \{L_{1}\sigma \})\cup (C_{2}\sigma \setminus \{{\overline {L_{2}\sigma }}\})

ここで、 $C_{1}\sigma ,C_{2}\sigma$ などは、それぞれの節やリテラルに代入 $\sigma$ を行ったものを表わす。

例

以下の節からの導出を考える。

C_{1}=\lnot P(x)\lor \lnot Q(y)\lor R(x,y)

C_{2}=Q\left(a\right)

C_{3}=P\left(b\right)

Q を単一化する代入 $\left\{y/a\right\}$ により $C_{1}$ と $C_{2}$ の導出を行うと、

C_{R}=\lnot P(x)\lor R(x,a)

続いて、P を単一化する代入 $\left\{x/b\right\}$ により $C_{R}$ と $C_{3}$ の導出を行うと、

C_{S}=R\left(b,a\right)

を得ることができる。

反駁による証明

反駁（はんばく、英: refutation）とは、節の集合からの導出により空節 □ を導くことである。反駁については以下の定理が成り立つ。

節の集合 S が充足不能である必要十分条件は、節の集合 S からの導出により空節 □ が導けることである。

これはエルブランの定理を導出に応用したものになっている。

論理式 P が恒真であれば $\lnot P$ は充足不能（恒偽）であるため、節の集合に $\lnot P$ を追加し導出を繰り返すことで空節 □ になれば、論理式 P が恒真であることが証明できる。

反駁により $P$ が $P_{1},\dots ,P_{n}$ の論理的帰結か調べるアルゴリズムは以下のように表現できる。

$P_{1},\dots ,P_{n}$ をスコーレム連言標準形 $C_{1},\dots ,C_{n}$ に変換する。
$\lnot P$ をスコーレム連言標準形 $C$ に変換する。
もし $C,C_{1},\dots ,C_{n}$ の反駁が存在すれば、 $F$ は $P_{1},\dots ,P_{n}$ の論理的帰結である。

あるいは、別の表現をすれば、

$C,C_{1},\dots ,C_{n}$ が充足不能
$\lnot P,P_{1},\dots ,P_{n}$ が充足不能
$P_{1},\dots ,P_{n}$ の解釈が ${\mathit {T}}$ ならば $\lnot P$ の解釈は ${\mathit {F}}$
$P_{1},\dots ,P_{n}$ の解釈が ${\mathit {T}}$ ならば $P$ の解釈は ${\mathit {T}}$

例

以下の公式が成り立つ時、 $P\left(a\right)$ が成り立つかどうかを証明する場合を考える。反駁の対象となる論理式は以下の論理式に $\lnot P(a)$ を追加したものである。

$\forall x\ ((S(x)\lor T(x))\to P(x))$ ,
$\forall x\ (S(x)\lor R(x))$ ,
$\lnot R(a)$

最初の論理式は $(\forall x\ (S(x)\to P(x))\land (\forall x\ (T(x)\to P(x))$ と等価なため、次の2つの節で表現できる。

C_{1}=\lnot S(x)\lor P(x)

C_{2}=\lnot T(x)\lor P(x)

二番目の論理式は以下の節になる。

C_{3}=S(x)\lor R(x)

さらに三番目は以下の節になる。

C_{4}=\lnot R(a)

証明したい論理式の否定は以下の節である。

C_{5}=\lnot P(a)

これらの節 ${C_{1},C_{2},C_{3},C_{4},C_{5}}$ が反駁の対象となる節集合である。

$C_{3}$ と $C_{4}$ の $R$ についての導出を考えると、 $\left\{x/a\right\}$ の代入により以下が導かれる。

C_{6}=S\left(a\right)

C_{1}

と

C_{6}

の

S

についての導出を考えると、

C_{7}=P\left(a\right)

最後に $C_{5}$ と $C_{7}$ の導出により空節 □ が導かれ、 $P\left(a\right)$ が成り立つことを証明できる。

証明戦略

導出は２つの節を前提として導出節を導くものであるので、どの節に導出規則を適用するかについてはさまざまな選択肢があり、そのやり方により効率が大幅に異なる。代表的な証明戦略として以下のものがある。

線形導出（linear resolution）
入力導出（input resolution）
支持集合戦略（set-of-support strategy）
意味導出（semantic resolution）

参考文献

J. Alan Robinson. "A Machine-Oriented Logic Based on the Resolution Principle." J. Assoc. Comput. Mach. 12, pp.23-41, 1965.
Davis Martin. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.
Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648.
Robert Kowalski. Logic for Problem Solving. North Holland, Elsevier, 1979.　ISBN 978-0444003683
Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers
佐藤泰介. 導出原理による定理証明. 情報処理 22(11), pp.1024-1036, 1981.

脚注

^ J. Alan Robinson, A Machine-Oriented Logic Based on the Resolution Principle. JACM, Volume 12, Issue 1, pp. 23–41. 1965.
^ Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.
^ ^a ^b Martin Davis. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan J.A. Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498
^ Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648

外部リンク

Alex Sakharov. "Resolution Principle". mathworld.wolfram.com (英語).
Alex Sakharov. "Resolution". mathworld.wolfram.com (英語).
Notes on computability and resolution (pdf)
述語論理とその意味論 (pdf) 筑波大学講義資料

[Robinson1965-1] J. Alan Robinson, A Machine-Oriented Logic Based on the Resolution Principle. JACM, Volume 12, Issue 1, pp. 23–41. 1965.

[Buss1995-2] Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.

[Davis2001-3] Martin Davis. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan J.A. Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498

[Bibel2007-4] Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648

[1]

[2]

[3]

[4]

@@ 1行目: / 1行目: @@
+'''導出'''（どうしゅつ、{{lang-en-short|''resolution''}}）とは、[[数理論理学]]における一つの[[演繹]]方法で、三段論法を一般化した導出規則と呼ばれるただ１つの推論規則を用いる。[[命題論理]]、[[述語論理]]のいずれにも使う事ができ、導出を繰り返すことで証明したい論理式の否定から空節が導かれることにより証明を行う。導出規則と[[単一化]]にもとづく'''導出原理'''（どうしゅつげんり、{{lang-en-short|''resolution principle''}}）は{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}により1965年に提案され<ref name=Robinson1965>J. Alan Robinson, ''A Machine-Oriented Logic Based on the Resolution Principle''. JACM, Volume 12, Issue 1, pp. 23–41. 1965.</ref>、
-'''導出'''（どうしゅつ）とは、[[数理論理学]]における一つの[[演繹]]方法である。[[定理自動証明]]において一般的に使われる手法。
+その後の[[定理自動証明]]に大きな影響を与え、また[[Prolog]]などの[[論理プログラミング]]言語の基礎となった。
+== 背景 ==
-導出おいて二つの[[節]]より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の[[論理和]]をとることで、新しい節を得ることをいう。式で表せば、命題<math>a_i</math>が命題<math>b_j</math>の否定である時、
+述語論理式 ''P'' が[[恒真式|恒真]]であるかを証明する一般的な手続きは存在しないが、1930年に発表された[[エルブランの定理]]は[[エルブランの定理#エルブラン領域|エルブラン領域]]の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、<math>\lnot P</math> が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には[[単一化]]アルゴリズムなど他のさまざまなものが含まれていた<ref name=Buss1995>Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.</ref>。
+年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)や[[:en:Davis–Putnam algorithm|デービス・パットナムのアルゴリズム]](1958,1960) が考案された。 これらはエルブランの定理の証明を直接計算機上で実現したような方法で、[[エルブランの定理#エルブラン領域|エルブラン領域]]の要素を順次生成して変数を含まない論理式(''基礎例'')を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった<ref name=Davis2001>Martin Davis. ''The Early History of Automated Deduction''. in ''Handbook of Automated Reasoning'', Volume I, Alan J.A. Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498</ref>。
+プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入（[[単一化]]）によって充足不能性を調べる方法を1960年に提案した<ref name=Bibel2007>Wolfgang Bibel. ''Early History and Perspectives of Automated Deduction''. in ''Advances in Artificial Intelligence'', 	Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648</ref>。
+この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形はすべての連言項を調べなければならないため全体の効率はいいとは言えなかった。
+ロビンソンはデービス・パットナムの枠組みにプラウィツのアイデアを組み合わせ、ただ１つの導出規則と[[単一化]]による代入操作とで充足不能性を調べる導出原理を1965年に発表した。単純な規則で関係する論理式のみを段階的に具体化していく方法は、従来の方法よりはるかに効率がよく、また理論的なエレガントさを持っていたためで、その後の[[定理自動証明]]に大きな影響を与えた<ref name=Davis2001></ref>。
+== 定義 ==
+''導出''とは二つの[[節]]より新しい節を導きだす操作で、一方の節に含まれるリテラル <math>l</math> と、他方の節に含まれる否定リテラル <math>\neg l</math> をのぞき、その他のリテラルの[[論理和]]をとることで、新しい節を得ることをいう。
+命題論理での導出規則を式で表せば、
 <math>\frac{
+l \vee P,
-a_1 \lor \ldots \vee a_{i-1} \vee a_i \vee a_{i+1} \vee \ldots \lor a_n,
+\quad \neg l \vee Q}
-\quad b_1 \lor \ldots \vee b_{j-1} \vee b_j \vee b_{j+1} \vee \ldots \lor b_m}
+{P \vee Q}</math>
-{a_1 \lor \ldots \lor a_{i-1} \lor a_{i+1} \lor \ldots \lor a_n  \lor  b_1 \lor \ldots \lor b_{j-1} \lor b_{j+1} \lor \ldots \lor b_m}</math>
+と書ける。ここで上式は前提となる節、下式はそれらから導かれる''導出節''（{{lang|en|''resolvent''}}）を表わす。
+あるいは、別の表記法を用いれば、前提となる節を <math>C_1</math> と <math>C_2</math> とし, もしリテラル <math>L \in C_1</math> と否定リテラル <math>\overline{L}\in C_2</math>  が存在すれば、導出節 <math>C_R</math> は以下のようになる。
-と書ける。
+:<math>
-導出は与えられた節の集合に、導出原理を当てはめ得られる新しい節をもとの節の集合に加える事を繰り返す事で行われる。[[命題論理]]、また[[述語論理]]いずれにも使う事が出来る。命題論理における導出は完全である。
+C_R = (C_1 \setminus\{L\}) \cup (C_2 \setminus \{\overline{L}\})
+</math>
+これは[[三段論法]]や[[モーダスポネンス|前件肯定]]を一般化した規則となっている。
-[[プログラミング言語]]の[[Prolog]]の基礎となる理論である。
+導出は[[完全性|完全]]な証明系であることが知られている。
+=== 例 ===
+<math> p \to q </math> を節形式にすると <math> \lnot p \lor q  </math> となる。<math> C_R </math> を<math> C_1, C_2 </math> の導出節とすると、[[モーダスポネンス|前件肯定]]は以下の導出と同じである。
+:<math> \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} </math>
+同様に、<math> p \to q </math>、<math> q \to r </math> の節形式 <math> \lnot p \lor q </math>、 <math> \lnot q \lor r </math> による[[三段論法]]は以下のようになる。
+:<math> \begin{array}{ll}
+C_1 = \lnot p \lor q & \left( p \to q \right) \\
+C_2 = \lnot q \lor r & \left( q \to r \right) \\
+C_R = \lnot p \lor r & \left( \mathrm{resolvent,\ }p \to r \right)
+\end{array} </math>
+== 一階述語論理での導出 ==
+述語論理のリテラルには個体変数が含まれるため、リテラルと否定リテラルとを単純に比較するだけでは削除できるかどうか分からない。一階述語論理ではリテラルと否定リテラルそれぞれの[[原子論理式]]が[[ユニフィケーション|単一化]]できる場合に導出を行う。
+また、導出の対象となる節は、[[冠頭標準形]]にして[[存在記号]]を削除した[[スコーレム標準形|スコーレム連言標準形]]の論理式である。
+例えば、一方の節がリテラル <math>p(x, y)</math>、もう一方の節がリテラル <math>\lnot p(z, f(b))</math> を含む場合、適切な代入 <math>\sigma =\left\{ z/x, y/f(b) \right\}</math> により各リテラルは <math>p(x, f(b))</math>、 <math>\lnot p(x, f(b))</math> と書き換えられ、同じにすることができる。ここで代入 <math>\left\{ z/x, y/f(b) \right\}</math> は <math>z \to x</math>、<math>y \to f(b)</math> に書き換えることを表わす。
+一般に論理式 <math>F_1, F_2</math> を等しくする代入を <math>F_1, F_2</math> の''単一化子''（{{lang|en|''unifier''}}）といい、そのうち最も一般的な単一化子（''最汎単一化子''）を <math>F_1, F_2</math> の''mgu''（{{lang|en|''most general unifier''}}）という。
+上記の例の場合、両方の論理式を等しくする代入は <math>\left\{ z/a, y/f(b), x/a \right\}</math>、<math>\left\{ z/x, y/c, f(b)/c \right\}</math> など無数に存在する。これらは本来の代入 <math>\left\{ z/x, y/f(b) \right\}</math> に <math>\left\{ x/a \right\}</math> などの代入を合成したものなので、最汎単一化子 mgu は <math>\left\{ z/x, y/f(b) \right\}</math> である。
+一階述語論理での導出は次のように表現できる。
+もしリテラル <math>L_1 \in C_1</math> と否定リテラル <math>\overline{L_2}\in C_2</math> が存在し、 <math>L_1</math> と <math>L_2</math> が mgu <math>\sigma</math> を持つ場合、以下の <math>C_R</math> を節 <math>C_1</math> と <math>C_2</math> との''２項導出節''という。
+:<math>
+C_R = (C_1\sigma \setminus\{L_1\sigma\}) \cup (C_2\sigma \setminus \{\overline{L_2\sigma}\})
+</math>
+ここで、<math>C_1\sigma, C_2\sigma</math> などは、それぞれの節やリテラルに代入 <math>\sigma</math> を行ったものを表わす。
+=== 例 ===
+以下の節からの導出を考える。
+:<math> C_1 = \lnot P (x) \lor \lnot Q (y) \lor R (x, y) </math>
+:<math> C_2 = Q \left(a \right) </math>
+:<math> C_3 = P \left(b \right) </math>
+''Q'' を単一化する代入 <math>\left\{y/a\right\}</math> により <math> C_1 </math> と <math> C_2 </math>の導出を行うと、
+:<math> C_R = \lnot P (x) \lor R (x, a) </math>
+続いて、''P'' を単一化する代入 <math>\left\{ x/b \right\}</math> により <math> C_R </math> と <math> C_3 </math>の導出を行うと、
+:<math> C_S = R \left(b, a \right) </math>
+を得ることができる。
+== 反駁による証明 ==
+'''反駁'''（はんばく、{{lang-en-short|''refutation''}}）とは、節の集合からの導出により空節 □ を導くことである。
+反駁については以下の定理が成り立つ。
+ 節の集合 ''S'' が充足不能である必要十分条件は、節の集合 ''S'' からの導出により空節 □ が導けることである。
+これは[[エルブランの定理]]を導出に応用したものになっている。
+論理式 ''P'' が[[恒真式|恒真]]であれば <math>\lnot P</math> は充足不能（恒偽）であるため、節の集合に <math>\lnot P</math> を追加し導出を繰り返すことで空節 □ になれば、論理式 ''P'' が[[恒真式|恒真]]であることが証明できる。
+反駁により <math>P</math> が <math>P_1, \dots ,P_n</math> の論理的帰結か調べるアルゴリズムは以下のように表現できる。
+# <math>P_1, \dots ,P_n</math> を[[スコーレム標準形|スコーレム連言標準形]] <math>C_1, \dots ,C_n</math> に変換する。
+# <math>\lnot P</math> を[[スコーレム標準形|スコーレム連言標準形]] <math>C</math> に変換する。
+# もし <math>C, C_1, \dots ,C_n</math> の反駁が存在すれば、 <math>F</math> は <math>P_1, \dots ,P_n</math> の論理的帰結である。
+::あるいは、別の表現をすれば、
+::* <math>C, C_1, \dots ,C_n</math> が充足不能
+::* <math>\lnot P, P_1, \dots ,P_n</math> が充足不能
+::* <math>P_1, \dots ,P_n</math> の解釈が <math>\mathit{T}</math> ならば <math>\lnot P</math> の解釈は <math>\mathit{F}</math>
+::* <math>P_1, \dots ,P_n</math> の解釈が <math>\mathit{T}</math> ならば <math>P</math> の解釈は <math>\mathit{T}</math>
+=== 例 ===
+以下の公式が成り立つ時、<math>P\left(a\right)</math> が成り立つかどうかを証明する場合を考える。反駁の対象となる論理式は以下の論理式に <math>\lnot P(a)</math> を追加したものである。
+# <math>\forall x \ ((S(x) \lor T(x)) \to P(x))</math>,
+# <math>\forall x \ (S(x) \lor R(x))</math>,
+# <math>\lnot R(a)</math>
+最初の論理式は <math>(\forall x \ (S(x) \to P(x)) \land (\forall x \ (T(x) \to P(x))</math> と等価なため、次の2つの節で表現できる。
+:<math>C_1 = \lnot S(x) \lor P(x)</math>
+:<math>C_2 = \lnot T(x) \lor P(x)</math>
+二番目の論理式は以下の節になる。
+:<math>C_3 = S(x) \lor R(x)</math>
+さらに三番目は以下の節になる。
+:<math>C_4 = \lnot R(a)</math>
+証明したい論理式の否定は以下の節である。
+:<math>C_5 = \lnot P(a)</math>
+これらの節 <math>{C_1, C_2, C_3, C_4, C_5}</math> が反駁の対象となる節集合である。
+<math>C_3</math> と <math>C_4</math> の <math>R</math> についての導出を考えると、<math>\left\{ x/a \right\}</math> の代入により以下が導かれる。
+:<math>C_6 = S \left(a \right)</math>
+:<math>C_1</math> と <math>C_6</math> の <math>S</math> についての導出を考えると、
+:<math>C_7 = P\left(a\right)</math>
+最後に <math>C_5</math> と <math>C_7</math> の導出により空節 □ が導かれ、<math>P\left(a\right)</math> が成り立つことを証明できる。
+== 証明戦略 ==
+導出は２つの節を前提として導出節を導くものであるので、どの節に導出規則を適用するかについてはさまざまな選択肢があり、そのやり方により効率が大幅に異なる。代表的な証明戦略として以下のものがある。
+* 線形導出（{{lang|en|''linear resolution''}}）
+* 入力導出（{{lang|en|''input resolution''}}）
+* 支持集合戦略（{{lang|en|''set-of-support strategy''}}）
+* 意味導出（{{lang|en|''semantic resolution''}}）
 == 関連項目 ==
 * [[エルブランの定理]]
 * [[スコーレム標準形]]
+* [[定理自動証明]]
+* [[論理プログラミング]]
+== 参考文献 ==
+*J. Alan Robinson. "A Machine-Oriented Logic Based on the Resolution Principle." J. Assoc. Comput. Mach. 12, pp.23-41, 1965.
+*Davis Martin. ''The Early History of Automated Deduction''. in ''Handbook of Automated Reasoning'', ''Volume I'', Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.
+*Wolfgang Bibel. ''Early History and Perspectives of Automated Deduction''. in ''Advances in Artificial Intelligence'', Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648.
+* Robert Kowalski. ''Logic for Problem Solving''. North Holland, Elsevier, 1979.　ISBN 978-0444003683
+* {{cite book
+ | last = Gallier
+ | first = Jean H.
+ | title = Logic for Computer Science: Foundations of Automatic Theorem Proving
+ | publisher = Harper & Row Publishers
+ | year = 1986
+ | url = http://www.cis.upenn.edu/~jean/gbooks/logic.html
+}}
+*佐藤 泰介. ''[http://ci.nii.ac.jp/naid/110002761456 導出原理による定理証明]''. 情報処理 22(11), pp.1024-1036, 1981.
+== 脚注 ==
+<div class="references-small">
+<references/>
+</div>
+== 外部リンク ==
+* {{MathWorld | urlname=ResolutionPrinciple | title=Resolution Principle | author=Alex Sakharov}}
+* {{MathWorld | urlname=Resolution | title=Resolution | author=Alex Sakharov}}
+* [http://www.cs.uu.nl/docs/vakken/pv/resources/computational_prop_of_fol.pdf Notes on computability and resolution] (pdf)
+* [http://www.score.is.tsukuba.ac.jp/~minamide/notes/note.pdf 述語論理とその意味論] (pdf) 筑波大学講義資料
 {{DEFAULTSORT:とうしゆつ}}
 [[Category:推論規則]]
-[[Category:数学基礎論]]
+[[Category:論理学]]
+[[Category:数理論理学]]
 [[Category:形式手法]]
 [[Category:数学に関する記事]]