命題論理のResolutionと証明について

命題論理のResolutionの基本的な例から、Resolutionで証明を構成する方法について考える。

概要

矛盾から何も証明できないのは、矛盾のリテラル数が0だったからなわけだが、リテラルが1個でもresolutionは適用できない。つまり

Σ = {+P}

のとき、clause +Pにはリテラルが1つしかなく、Σにはclauseが1つしかないので resolutionは適用できず

 +P⊢+P

を導くことができない。

Gentzen流などでは証明の出発点が A⇒Aなので、こういうことは問題にならない。

Resolutionは不完全なのだろうか。

そんなことはなくて、たぶん、Resolutinは反証法(帰謬法とか背理法とか)によって証明することが前提の推論規則なのだと思う。

反証法では、+P⊢+Pを証明しようと思う時、右辺の+Pを否定した-Pを作り、これと左辺を合わせて、そこから矛盾を証明しようとする。

+P, -P ⊢□

これはresolutionの1stepの証明ができる。このとき、前提としていた-Pが間違っていたので、

+P⊢+P

が正しいという結論に至る。

これによって、Σ⊢Aは、resolutionでも証明できるようになる。反証法を使わないとGentzen流の古典論理と同等にはならないということかな。

[補足]
1) Σ⊢Γに対して反証法を使うためには、
 (1) Σが無矛盾
 (2) Γが無矛盾
 (3) 推論規則が無矛盾なものから矛盾を導けない
ということが必要である。
 推論規則、この場合 Resolutionが矛盾していないというのは自明だろうか。よくわからない。 
2) clauseの否定の仕方については注意が必要。
3) 反証法を使うことにより、Γconjectureの否定に着目することで、証明したい命題に繋がりのある証明だけを構成することになる。
(補足おわり)

 ちなみに、clause Cに、+P, -Pが含まれる場合は、Σが1 clauseであっても、CとCのペアに対してresolutionを適用できる。ΣがN clauseでも同じこと。

例)
   +P∨-P  +P∨-P 
  ------------------
               +P∨-P 
となる。
 これが重要なのは述語論理のときなので、述語論理のresolutionについて説明した折にまた触れる。