導出原理

導出原理とは

導出原理（resolution principle）は、1965年にジョン・アラン・ロビンソンによって提案された、論理的な推論を行うための基本的な原理です。この原理は、特に定理の自動証明やPrologのような論理プログラミング言語において重要な役割を果たしています。

背景

述語論理式が常に真であるかを証明する一般的な方法は存在しません。しかし、1930年に発表されたエルブランの定理は、エルブラン領域の要素を論理式に代入し、命題論理のレベルでその充足不能性を検証することで、有限のステップで証明可能であることを示しました。エルブランの論文には、単一化アルゴリズムも含まれていました。

1950年代以降、計算機上での定理証明の研究が盛んになり、ギルモアのアルゴリズムやデービス・パトナムのアルゴリズムが開発されました。これらのアルゴリズムは、エルブランの定理を直接的に計算機上で実現しようとするもので、エルブラン領域の要素を順次生成し、変数を含まない論理式を作成して充足不能性を調べるため、非常に非効率でした。

1960年、プラウィツは、論理式を生成する前に、選言標準形に変換した論理式への適切な代入（単一化）によって充足不能性を調べる方法を提案しました。この方法は、必要な基礎例のみを生成するため効率的でしたが、選言標準形のすべての連言項を調べる必要があったため、全体の効率はまだ課題でした。

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

定義

導出とは、二つの節から新しい節を導き出す操作です。具体的には、一方の節に含まれるリテラル \( l \) と、他方の節に含まれる否定リテラル \(
eg l \) を除き、残りのリテラルの論理和を取ることで新しい節を得ます。

命題論理における導出規則は、以下のように表現できます。

math
\frac{l \lor P, \quad
eg l \lor Q}{P \lor Q}


ここで、上式は前提となる親節、下式は導出される導出節（resolvent）を表します。

別の表記法を用いると、前提となる節を \( C_1 \) と \( C_2 \) とした場合、リテラル \( L \in C_1 \) と否定リテラル \( \overline{L} \in C_2 \) が存在するならば、導出節 \( C_R \) は次のようになります。

math
C_R = (C_1 \setminus \{L\}) \cup (C_2 \setminus \{\overline{L}\})


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

例

例えば、\( p \to q \) を節形式に変換すると \(
eg p \lor q \) となります。このとき、前件肯定は以下の導出と同じです。

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}


同様に、\( p \to q \) と \( q \to r \) の節形式 \(
eg p \lor q \) と \(
eg q \lor r \) による三段論法は以下のようになります。

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}

一階述語論理での導出

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

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

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

一般に、論理式 \( F_1, F_2 \) を等しくする代入を単一化子（unifier）といい、最も一般的な単一化子をmgu（most general unifier）といいます。上記の例では、mguは \( \{z/x, y/f(b)\} \) となります。

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

もしリテラル \( L_1 \in C_1 \) と否定リテラル \( \overline{L_2} \in C_2 \) が存在し、\( L_1 \) と \( L_2 \) がmgu \( \sigma \) を持つ場合、以下の \( C_R \) が2項導出節（binary resolvent）です。

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


同様の方法で、複数の節から同時に導出することも可能であり、超導出（hyper-resolution）と呼ばれます。

例として、以下の節からの導出を考えます。

math
\begin{array}{ll}C_1 = \lnot P(x)\lor \lnot Q(y)\lor R(x,y)\\C_2 = Q(a)\\C_3 = P(b)\end{array}


\( Q \) を単一化する代入 \( \{y/a\} \) により、\( C_1 \) と \( C_2 \) の導出を行うと、

math
C_R = \lnot P(x) \lor R(x,a)


続いて、\( P \) を単一化する代入 \( \{x/b\} \) により \( C_R \) と \( C_3 \) の導出を行うと、

math
C_S = R(b,a)


が得られます。

反駁による証明

反駁（refutation）とは、節の集合からの導出により空節 □ を導くことです。反駁に関しては以下の定理が成立します。

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

これはエルブランの定理を導出に応用したものです。

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

反駁を利用して、\( P \) が \( P_1, \dots, P_n \) の論理的帰結かを調べるアルゴリズムは以下のようになります。

1. \( P_1, \dots, P_n \) をスコーレム連言標準形 \( C_1, \dots, C_n \) に変換します。
2. \(
eg P \) をスコーレム連言標準形 \( C \) に変換します。
3. もし \( C, C_1, \dots, C_n \) の反駁が存在すれば、\( P \) は \( P_1, \dots, P_n \) の論理的帰結です。

例えば、 \( \forall x \ ((S(x)\lor T(x))\to P(x)) \) , \( \forall x \ (S(x)\lor R(x)) \), \(
eg R(a) \) が成り立つ時に、\( P(a) \) が成り立つかを証明する場合を考えます。反駁の対象となる論理式は以下の節集合になります。

math
\begin{array}{ll}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)\end{array}


これらの節から導出を繰り返すと最終的に空節が導かれ、\( P(a) \) が成り立つことが証明されます。

証明戦略

導出は、どの節に導出規則を適用するかによって効率が大きく異なります。代表的な証明戦略には以下のようなものがあります。

線形導出（linear resolution）: 導出の流れが線状に一列に並ぶように、頂上節とそこから導出された節を前提とします。PrologのSLD導出はこの一種です。
入力導出（input resolution）: 前提となる節の一方を、最初に与えられた節集合の要素に限定します。
支持集合戦略（set-of-support strategy）: あらかじめ指定された支持集合の節と、そこから導出された節を前提とします。これにより、無関係な探索を避けて効率的な導出を可能にします。
意味導出（semantic resolution）: 論理式のモデルや解釈を利用して導出の対象を制限し、探索空間を狭めます。例えば、特定のモデルにおいて真となる節と偽となる節を親節に選ぶ方法があります。

これらの戦略を用いることで、導出原理をより効率的に活用することが可能です。

参考文献

長尾 真、淵 一博『論理と意味』 7巻、岩波書店〈岩波講座 情報科学〉、1983年。
山崎 進『計算論理に基づく推論ソフトウェア論』コロナ社、2000年。
D.ヒルベルト、W.アッケルマン 著、伊藤誠（訳） 編『記号論理学の基礎』大阪教育図書社、1954年。
Robert Kowalski (1974), Predicate Logic as Programming Language
Wolfgang Bibel (2007), “Early History and Perspectives of Automated Deduction”
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.
Robert Kowalski. Logic for Problem Solving. North Holland, Elsevier, 1979.
Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.
佐藤 泰介. 導出原理による定理証明. 情報処理 22(11), pp.1024-1036, 1981.

外部リンク

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

もう一度検索