導出原理 導出原理の概要

ウィキペディア

導出原理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/10/21 06:25 UTC 版)

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

背景

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

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

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

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

定義

導出とは二つの節より新しい節を導き出す操作で、一方の節に含まれるリテラル $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\}$ である。

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

もしリテラル $L_{1}\in C_{1}$ と否定リテラル ${\overline {L_{2}}}\in C_{2}$ が存在し、 $L_{1}$ と $L_{2}$ が mgu $\sigma$ を持つ場合、以下の $C_{R}$ が2項導出節（binary resolvent）である。ここで、$C_{1}\sigma ,C_{2}\sigma$ などは、それぞれの節やリテラルに代入 $\sigma$ を行ったものを表す。

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

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

例

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

$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)$

を得ることができる。