resolution(命題論理)

　論理体系のシステムとして、Gentzen流やHilbert流(なぜ「流」というのかは謎)がある。J.A.Robinsonは Resolutionという推論規則を持つ論理体系を考案した。ここではそれをRobinson流と呼ぶことにする。
(Gentzen流やHilbert流については教科書やWikipediaの説明を見てください)

まず、命題論理でのResolution推論規則について説明する。述語論理のResolutionはこれの上に成り立っている。

命題論理のResolutionで対象とする論理式は次のようなものになる。

1) literal: atomicな論理式かその否定の形をしたもの。「リテラル」と書くことも。
　「atomicな論理式」と言っているのは、論理記号(¬、∨、∧、⇒、⇔などを使っていない論理式)のこと。

　　例　Pを命題変数(記号)として +Pや-P
　以下では、否定と否定でないものを区別したいので、+と-をつけている。普通はPと¬Pのようにaffirmativeな方は符号をつけないで書く。
　ただし、+/-をつける表記はliteralを具体的に書くときの方法で、一般的に論理式について考えている場合、否定を¬で表し、「命題Aの否定は¬A」のように書く。混乱することはないと思う。
　また、このリテラルに対して、符号(+/-)を除いた命題変数の部分は「リテラルのアトミックな部分」と呼ぶことにする。(ここは普通の教科書などと違うように思う)

2) clause: literalの集合
　　例 {+P, -R, +S}
　　これは∨で繋げられているとみなす。つまりこの例は次の論理式と同じ。
　　+P∨-R∨+S
　　集合としてのclauseの{}は略すことが多く、上の例は、
　　　+P-R+S
　　とも書く。足したり引いたりしているようにも見えるが、間違うことはないだろう。

3) clause集合: clauseの集合
　　例{+P-R+S, -P, -R+Q}
　clause集合は、∧でつなげた論理式とみなす。つまり例の集合は
　　　(+P-R+S)∧-P∧(-R+Q)
　を表す。

　古典論理では、任意の論理式をそれと同値な冠頭標準形(ド・モルガン則、二重否定の除去などを使用)に変換できるが、この冠頭標準形はclause集合と1対1対応すると解釈できる。

* clauseでは+、-、∨と∧しかでてこないが、話の都合ででてくるかもしれない論理記号は、次のような記号を用いる。

A ⇒ B　AならばB
A ⇔ B　AはBと同値

[その他の記法]
 - A ⊢ Bで、Aを仮定してBが正しいということの証明を表すことにする。
 - □で矛盾を表すことにする。
- resolutionでは、clauseとしての矛盾は∅であり、0個のリテラルを持つclauseである。∅-clauseと書いてもよいかもしれないと思う。empty clauseという言い方はあるのでこの言い方も間違いではないだろう。

[Resolution]

[推論規則]

Pを命題変数、α、 βをliteralの並びとして、Resolution規則は、次のようなルールである。

　+P∨α  -P∨β
 —----------------- 
　　　α∨β

上の二つの論理式が真なら下の式も真になることは、命題論理の場合、真偽表などで確認できる。古典論理を知っている人なら、直感的には、¬P∨QとP⇒Qが同値であることからもわかる。

resolutionを適用して得られたclause α∨βをresolventと呼ぶ。

ちなみに、clauseは集合なので、resolventが{+P, +P, -R}という形になることはなく、同じ要素は削除し、{+P, -R}となる。自動証明のようにプログラムで実行する場合、推論規則とは別に集合としての処理が必要になり、推論規則としては扱われない。

[証明]

clauseの集合Σと定理Zについて、resolutionを用いた証明Σ⊢Zとは、大雑把にいってΣからZにいたるresolutionの連鎖のことになる。

もうすこし説明を試みると、まず、次のようなclauseの並びを考える。

この並びは、Σの要素のclauseから出発し、この並びの要素同志のresolventが得られたらそれを列に追加する。というように生成される。そして、列にZが追加されたら、完成とする。

この列にはZを証明するために必要のないclauseも含まれるので、Σの要素clauseからresolventZに至るに必要なclauseとresolventだけを取り出したものを「ΣからZの証明」と呼ぶ。

厳密な定義は教科書などを参照してください。