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

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

インライン

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

導出（どうしゅつ、英: 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}$ の反駁が存在すれば、 $P$ は $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]

@@ 97行目: / 97行目: @@
 # <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>P</math> は <math>P_1, \dots ,P_n</math> の論理的帰結である。
 ::あるいは、別の表現をすれば、
 ::* <math>C, C_1, \dots ,C_n</math> が充足不能