導出原理のソースを表示

'''導出原理'''（どうしゅつげんり、{{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]]などの[[論理プログラミング]]言語の基礎となった。

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

1950年代以降、計算機上での定理証明の研究が活発になり、[[ギルモアのアルゴリズム]](1960)や[[デービス・パトナムのアルゴリズム]](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>。
この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形は全ての連言項を調べなければならないため全体の効率はいいとは言えなかった。

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

== 定義 ==
''導出''とは二つの[[ホーン節|節]]より新しい節を導き出す操作で、一方の節に含まれるリテラル <math>l</math> と、他方の節に含まれる否定リテラル <math>\neg l</math> をのぞき、その他のリテラルの[[論理和]]をとることで、新しい節を得ることをいう。

[[命題論理]]での導出規則を式で表せば、
<math>\frac{
l \vee P, 
\quad \neg l \vee Q}
{P \vee Q}</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>

導出規則は[[三段論法]]や[[モーダスポネンス|前件肯定]]を一般化した規則となっている。
導出は[[完全性|完全]]な証明系であることが知られている。

=== 例 ===
<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> である。

一階述語論理での導出は mgu を用いて次のように表現できる。

もしリテラル <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> が''2項導出節''（{{lang|en|''binary resolvent''}}）である。ここで、<math>C_1\sigma, C_2\sigma</math> などは、それぞれの節やリテラルに代入 <math>\sigma</math> を行ったものを表す。

:<math>
C_R = (C_1\sigma \setminus\{L_1\sigma\}) \cup (C_2\sigma \setminus \{\overline{L_2\sigma}\})
</math>

同様のやり方での2以上の複数の節から同時に導出することも可能であり、''超導出''（{{lang|en|''hyper-resolution''}}）と呼ばれる。
=== 例 === 
以下の節からの導出を考える。

:<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''}}）とは、節の集合からの導出により空節 □ を導くことである。
反駁については以下の定理が成り立つ。
<blockquote class="toccolours" style="text-align:justify; width:50%; float:center; padding: 10px; display:table; margin-left:80px;">
節の集合 ''S'' が充足不能である必要十分条件は、節の集合 ''S'' からの導出により空節 □ が導けることである。
</blockquote>
これは[[エルブランの定理]]を導出に応用したものになっている。

論理式 ''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>P</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>

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

:<math>C_3 = S(x) \lor R(x)</math>

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

:<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|''top clause''}}）として指定した節と、頂上節から導出された節に限定する方法。導出木を書くと導出の流れが線状に一列に並ぶため、線形導出と呼ばれる。[[論理プログラミング]]言語の代表である[[Prolog]]で用いられる''SLD導出''（{{lang|en|''Selective Linear resolution for Definite clause''}}）は線形導出の一種である。
* 入力導出（{{lang|en|''input resolution''}}）
:前提となる節の一方を最初に与えられた節集合の要素（導出された節以外の節）に限定する方法。
* 支持集合戦略（{{lang|en|''set-of-support strategy''}}）
:あらかじめ支持集合という節の集合を指定しておき、前提となる節の一方を支持集合の節とそこから導出された節に限定する方法。節集合''S''、''T'' があり''S-T'' が充足可能であるとき''T'' は''S'' の支持集合と言う。目標に関係ないところを探索しないよう導出の対象を制限することで、より効率的な導出を行うための手法で、1965年に Lawrence Wos らが提案した<ref>
Lawrence Wos, G.A. Robinson, D.F. Carson. ''Efficiency and Completeness of the Set of Support Strategy in Theorem Proving''. Journal of the ACM, Volume12, Issue 4, pp.536-541. 1965.</ref>。
* 意味導出（{{lang|en|''semantic resolution''}}）
:論理式のモデルあるいは解釈を利用して導出の対象を制限し、探索の空間を狭めることで効率的な導出を行う手法。特定のモデルにおいて真となる可能性がある節と偽となる可能性のある節とを親節に選ぶ Slagle の Semantic Clash resolution<ref>
James Slagle. ''Automatic Theorem Proving With Renamable and Semantic Resolution''. Journal of the ACM, Volume14, Issue 4, pp.687-697. 1967.</ref> など様々な方法がある。

== 脚注 ==
<div class="references-small">
<references/>
</div>

== 関連項目 ==
{{col-begin}}
{{col-break}}
* [[数理論理学]]
** [[命題論理]]
** [[述語論理]]
{{col-break}}
* [[自動定理証明]]
* [[論理プログラミング]]
* [[エルブランの定理]]
** [[ギルモアのアルゴリズム]]
** [[デービス・パトナムのアルゴリズム]]
** [[DPLLアルゴリズム]]
{{col-break}}
{{col-end}}

== 参考文献 ==
* {{cite book | 和書 | title=論理と意味 | author=長尾 真、淵 一博 | series=岩波講座 情報科学 | volume=7 | publisher=岩波書店 | year=1983 | ref=長尾(1983) }}
* {{cite book | 和書 | title=計算論理に基づく推論ソフトウェア論 | author=山崎 進 | year=2000 | publisher=コロナ社 | ref=山崎(2000) }}
* {{cite book | 和書 | author=D.ヒルベルト、W.アッケルマン | editor=伊藤誠（訳） | title=記号論理学の基礎 | year=1954 | publisher=大阪教育図書社 | ref=HA(1954) }}
* {{citation | author=Robert Kowalski | title=Predicate Logic as Programming Language | year=1974 | url=http://www.doc.ic.ac.uk/~rak/papers/IFIP%2074.pdf | ref=Kowalski(1974) }}
* {{citation | author=Wolfgang Bibel | chapter=Early History and Perspectives of Automated Deduction | title=Advances in Artificial Intelligence | series=Lecture Notes in Computer Science | publisher=Springer-Verlag Berlin | year=2007| url=http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf | ISBN=9783540745648 | ref=Bibel(2007) }}
*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.
* 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
}}
*佐藤 泰介. ''[https://cir.nii.ac.jp/crid/1050282812854402176 導出原理による定理証明]''. 情報処理 22(11), pp.1024-1036, 1981.

== 外部リンク ==
* {{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.cs.tsukuba.ac.jp/~minamide/notes/note.pdf 述語論理とその意味論] (pdf) 筑波大学講義資料


{{DEFAULTSORT:とうしゆつ}}
[[Category:推論規則]]
[[Category:命題論理の定理]]
[[Category:数理論理学]]
[[Category:形式手法]]
[[Category:数学に関する記事]]
[[Category:自動定理証明]]