導出原理

出典: フリー百科事典『ウィキペディア（Wikipedia）』
移動先: 案内、 検索

導出原理（どうしゅつげんり、テンプレート:Lang-en-short）とは、テンプレート:仮リンクにより1965年に提案された[1]原理または手法を言う。

導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。

背景

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

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

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

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

定義

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

命題論理での導出規則を式で表せば、 <math>\frac{ l \vee P, \quad \neg l \vee Q} {P \vee Q}</math> と書ける。ここで上式は前提となる親節、下式はそれらから導かれる導出節（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> の単一化子（unifier）といい、そのうち最も一般的な単一化子（最汎単一化子）を <math>F_1, F_2</math> のmgu（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項導出節（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以上の複数の節から同時に導出することも可能であり、超導出（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）とは、節の集合からの導出により空節 □ を導くことである。 反駁については以下の定理が成り立つ。

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

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

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

反駁により <math>P</math> が <math>P_1, \dots ,P_n</math> の論理的帰結か調べるアルゴリズムは以下のように表現できる。

  1. <math>P_1, \dots ,P_n</math> をスコーレム連言標準形 <math>C_1, \dots ,C_n</math> に変換する。
  2. <math>\lnot P</math> をスコーレム連言標準形 <math>C</math> に変換する。
  3. もし <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> を追加したものである。

  1. <math>\forall x \ ((S(x) \lor T(x)) \to P(x))</math>,
  2. <math>\forall x \ (S(x) \lor R(x))</math>,
  3. <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> が成り立つことを証明できる。

証明戦略

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

  • 線形導出（linear resolution）
前提となる節の一方を、頂上節（top clause）として指定した節と、頂上節から導出された節に限定する方法。導出木を書くと導出の流れが線状に一列に並ぶため、線形導出と呼ばれる。論理プログラミング言語の代表であるPrologで用いられるSLD導出（Selective Linear resolution for Definite clause）は線形導出の一種である。
  • 入力導出（input resolution）
前提となる節の一方を最初に与えられた節集合の要素（導出された節以外の節）に限定する方法。
  • 支持集合戦略（set-of-support strategy）
あらかじめ支持集合という節の集合を指定しておき、前提となる節の一方を支持集合の節とそこから導出された節に限定する方法。節集合S、T がありS-T が充足可能であるときT はS の支持集合と言う。目標に関係ないところを探索しないよう導出の対象を制限することで、より効率的な導出を行うための手法で、1965年に Lawrence Wos らが提案した[5]。
  • 意味導出（semantic resolution）
論理式のモデルあるいは解釈を利用して導出の対象を制限し、探索の空間を狭めることで効率的な導出を行う手法。特定のモデルにおいて真となる可能性がある節と偽となる可能性のある節とを親節に選ぶ Slagle の Semantic Clash resolution[6] など様々な方法がある。

脚注

  1. ↑ J. Alan Robinson, A Machine-Oriented Logic Based on the Resolution Principle. JACM, Volume 12, Issue 1, pp. 23–41. 1965.
  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.
  3. ↑ 3.0 3.1 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
  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
  5. ↑ 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.
  6. ↑ James Slagle. Automatic Theorem Proving With Renamable and Semantic Resolution. Journal of the ACM, Volume14, Issue 4, pp.687-697. 1967.

関連項目

テンプレート:Col-begin テンプレート:Col-break

テンプレート:Col-break

テンプレート:Col-break テンプレート:Col-end

参考文献

外部リンク

「http://wikippe.e-do-match.com/index.php?title=導出原理&oldid=9233」から取得