命題論理の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について説明した折にまた触れる。