resolution(述語論理)

矛盾については命題論理だけで話ができた。

ここでは、述語論理のresolutionについてまとめたい。

命題論理のresolutionでそうだったように、2つのclausesからresolventを作るという形式は述語論理でも変わらない。

見た目の違いといえば、命題論理ではPとかQとか書いていたことを、述語論理ではP(x,y)とかQ(f(a))とか引数をもつ表現まで拡張するところだろうか。
このようにxとかyという変数も使えるようになる。

変数については、限量子と呼ぶ記法がある。以下のように書く。

∀x,y.+P(x,y)　　任意のx,yについて+P(x,y)が成り立つことを言う。

∀x∃z.+P(x,z)　 任意のxについてあるzが存在し+P(x,z)が成り立つことを言う。

命題論理のときと同じような順番で、述語論理において、Resolutionで対象とする論理式を示していく。

1) literal: atomicな論理式かその否定の形をしたもの。
　　例　P、Rを述語記号、x、yを変数として +P(x), -R(x,y)
　ここでも、+,-と¬を使い分ける。
　リテラルのアトミックな部分について例で示すと、たとえば、リテラル +P(x)や-P(x)のアトミックな部分は「P(x)」になる。

2) clause: literalの集合
　　例 {+P(x), -R(x, y), +S(a)}
　　命題算と同様に、∨で繋がっているとみなすので、この例は次の論理式を意味する。
　　　+P(x)∨-R(x, y)∨+S(a)
　　clauseに出現する変数はclauseごとにすべて∀で束縛される。∨も省略して
　　　+P(x)-R(x, y)+S(a)
　と書く。

　この書き方では、x, y, aが変数なのか定数なのかわからなくて曖昧になっている。それでは困る、変数を明記したいという場合は、

　　(x, y).{+P(x),-R(x, y),+S(a)}や(x, y).+P(x)-R(x, y)+S(a)

　などのように書くことにする。慣習としてx, y, z, w, u, vなどは変数を表すために使うので、(x,y).の部分は省略させていただくこともあるだろう。中途半端な書き方だが、限量子∀を補って次のように書くこともあるかもしれない。

　∀x∀y.(+P(x)-R(x, y)+S(a))
　∀x, y(+P(x)-R(x, y)+S(a))

見てわかる時は随時簡略に書くだろう。

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

　また、述語論理の論理式もまた冠頭標準形へ変換できる。命題論理のときの変換ルールに加えて∀や∃、それらと¬に関する同値変換も使う。
　最終的な変形のあと、∀変数は全体を束縛していることになるが、∧をまたがる∀変数は同じ記号でも独立な(別々の)値をとりうるので、変数の束縛はclauseごとに行われると考えてよい。つまり別のclauseに同じ変数が出現しても、それらは別の変数(名)として扱う。(プログラムでresolutionを処理するときは、clauseごとに変数が異なるようにしてからresolutionをする)

この冠頭標準形は、clause集合と形は違うが、1対1対応するので、論理式をclause集合で代用できる。clause集合は自動証明で扱うのに便利だ。

用語
 - 一般に変数を含まない式をgroundなんとかという。ground clauseとかground termなどという言い方がある。しかし、日本語だとgroundという言葉はあまり使わないし文字数も多いので、0変数clauseとか0変数項などと呼ぶかもしれない。

- 項やリテラルなどを表現だと見たとき、表現としてあるいは文字列(厳密には違う)として同一だということを≡で表すことにする。たとえば 

　f(x,a)≡f(x,a)
　-(f(x,a)≡f(b,a))

[resolution(述語論理)]

[推論規則]
命題論理で、+Pと-Pを消してもよかったのは、Pの部分が完全に一致しているからである。
述語論理では事情が違う。
たとえば{+P(x), -P(a)}について考えてみよう。
述語論理でも、+P(a)と-P(a)の場合は無条件で矛盾するので消してもよいが、+P(b)と-P(a)では形が違い矛盾しないので、このままで二つのリテラルを消滅させ矛盾を導出してはならない。

消してもいい場合というのは{x=a}の条件を満たす場合だけで、この場合は二つのリテラルはきちんと矛盾するので、消しても良いと言えるわけだ。
つまり、x=aの場合に+P(x)と-P(a)は矛盾し、命題論理版resolutionが適用できる。それ以外の場合については、何も言えない。

このように、二つの式を矛盾させるため、表現を同一にする条件(今だと{x=a})を求めるアルゴリズムが存在し、unificationアルゴリズムと呼ばれる。単にunificationと言うかもしれない。(unificationアルゴリズムや代入については別の稿で書く)

上の例では条件を{x=a}という等式で書いたが、unificationはこの条件を代入という形で生成する。上の例だと{x←a}という代入になる。

つまり、リテラルL1とL2が符号は違うが同じ述語記号である場合、両方のatomicな部分を同一にする代入σをunificationアルゴリズムで求める。そのような代入が求められず、unificationに失敗する場合はresolutionを適用できない。あるいはresolutionに失敗すると言う。

補足
たとえば、述語論理のclauseがあるとき、その引数部分を消すと命題論理のclauseに見える。この命題論理レベルのclauseでresolutionが適用できない場合、unificationを考えるまでもなく述語論理でのresolutionは適用できない。
たとえば、+P(x)と-R(y)は、PとRが違うので命題論理でresolutionができず、故に述語論理でもresolutionできない。
+P(a)と-P(b)は+Pと-Pは同じPなので命題論理ではresolutionできるが、これはaとbをunificationできないので述語論理ではresolutionできない。

述語論理のresolutionは、変数に適切な項を代入して(その代入をσだとすると)、L1σ≡L2σとできるとき、L1σと¬L2σを対消滅させてもよいというルールである。(Lσはリテラルに代入σを適用した結果のこと) 同じ形にしたあとで見れば、同一のリテラルを対消滅させる命題論理のresolutionになっている。変数があるときも、同じ変数名なら同一とする。

このように二つの式を同じにすること、代入σを求めることをunifyするなどともいう。また、二つの表現を同じにする代入をunifierと呼ぶ。

さらに unificationアルゴリズムで求められる代入は「most general unifier」(略してmgu)と呼ばれる。
このmostの意味について簡単に説明する。二つの式L1とL2のmguをμとすると、L1とL2の任意のunifier σについて、L1σ がL1μのインスタンスになるようにμは作られる。この意味でμはL1とL2をunifyする「最も一般的」な代入になっている。それで「most」をつける。

ここだけの話だが、式tとsのunifierを<t:s>と書くことにする。
unificationに失敗すると、この表現が存在しない代入を示すことになるので、∃σ=<t:s>と書いて、存在するときだけσが代入になるという気持ちを表そうと思う。でも恥ずかしいのでこの表記はそれほど使わないだろう。

例) x,yを変数として、
　・<P(x,a):P(b,y)>=σ={x←b, y←a}が、P(b,a)にunifyする代入である。
　・<P(x,x):P(y,f(y))>は{x←f(x)}が必要となるが、これは代入の条件に反するのでmguは定義されない。(このように元のclauseに共通の変数がなくても、unificationでmguを求めるさいにvとtに共通の変数が登場することはある)

clauseに変数を指定する書き方は説明したが、unificationでも同様に変数を明記して次のように書く場合もある。ただし、だいたい変数がどれかはわかるので、簡潔に書きたいときは変数を明記しないで済ませる。また変数がない場合は、().と書いてもよいが、たぶん何も書かないだろう。

　 (x, y).<P(x, a):P(b, y)>
　
例) unify できない例(変数はx,y。定数はa,b)
  1) <P(a) : P(b)> : 定数aとbはunifyできない。代入が存在しない。
  2) <P(x, x) : P(z, f(z))>   :  これは{x←f(x)}のような代入が必要となるが、代入の定義からこれは不可であり、unifyできない。

このunificationの記法をresolutionに拡張して、やや乱暴だが、次のように書くこともあるが、混乱することはないと思う。あまりこれは書かないけれど。

　resolutionの場合: <+P(x):-P(a)>

[factoring]
また、たとえば、+P(a)∨+P(x)∨+R(x, x)というclauseは+P(a)∨+R(a, a)としてよい。<a:x>={x←a}を適用している。

ルールとして書くと、αをリテラルの集合としたときL1∨L2∨αのようなclauseで、L1とL2の述語記号と符号が同じ場合、L1とL2が代入σで同一になれば、(L1∨L2∨α)σからL2σを除去して(L1∨α)σとしてよいということになる。
この規則をfactoringと呼ぶ。
命題論理の場合は同じ状況でも、集合なので自動的に同じリテラルは1つだけになるが、述語論理では引数が異なって形の違うリテラルである場合でもunifyできるときはこのようにできる。
命題論理のレベルで考えるとclauseは集合だと考えているので、L1σとL2σが同一なら、命題算の場合と同じく、単に集合には同じ要素はひとつしかないから一つだけになるということだ。

一般的には、+P(a)∨+P(x)∨+R(x,x)を使って矛盾が求められるのであれば、factoringを適用しなくても、+P(a)を消すリテラルを導出する証明αがあれば、+P(x)もαを使って消滅させられるので、矛盾は求められるように思うが、このような例がありうる。

　{ +P(x)+P(y), -P(z)-P(w)}   … (1)

　この二つのclausesからは2リテラルのresolventしか作れないので、矛盾は導出できない。factoringを適用してはじめて矛盾が導ける。

まとめ
述語論理では、resolutionとfactoringの2つが推論規則である。

補足の補足
はっきり書いていなかったが、述語論理の論理式を命題論理とみなす方法を二つ使っている。
1) Σ中の P(…) を、引数を消してPという命題とみなす。
2) P(a,b)のように変数を含まないリテラルをまるごと命題とみなす。
　　変数があると、clauseが異なればすべて異なる変数と扱う必要があるので、変数名を書き換えると同一の形にはならないから、命題としてunifyできない。

述語論理の論理式を命題とみなすときは、たいてい1)を考えると思うが、2)の見なし方もときどき便利なので整理してみた。

また、関数がひとつもなく、引数の変数がすべて異なるようなliteralの場合、たとえば

　3) +P(x, y, z)と-P(w, u, v)

については、変数が何も制約条件になっていないので命題論理の範囲で扱える。