無矛盾の証明
反証法を使って Σ⊢Γ を示したいとき、ΣもΓもそれぞれ無矛盾でなくてはならない。そうでなければ、Σ, ¬Γ⊢□の証明が得られたとしても、たとえば、Σだけで矛盾が導出できるなら、それをΓの証明に変形することはできないからである。(最後に例をあげてみる)
(推論規則も矛盾していないことが必要)
では、clause集合Σが無矛盾であることはどうやって示せばよいのか?
ここでは二つの方法について考えてみる。とはいえ、もしもΣ⊢□が証明できたとしても、そのような証明が見つかるまでにどれくらいの時間がかかるかはわからないし、矛盾がそんざいしなければその手続は終わらないだろう。ただし、有限個のresolventで終了するような場合は、結果がわかる。それが役に立つ場合もある。
予備知識) Resolutionでは、goalとなるclause G を定めて、Σ, G⊢□の導出を目指す。
方法1 ∀c ∈ Σについて、Σ⊢cは自明なので、Σ⊢¬cを証明できれば矛盾することが示せる(かな?)。このΣには、goalGは含まない。
反証法を用いると、Σ, c ⊢□ を証明することになるが、Σ∋cなので、cをgoalとしてΣ⊢□をさがせばよい。ただし、単にΣから矛盾を導出するのでなく、goalをcと取れるので調べる範囲は限定されている。
しかし、Σ⊢□のとき、∃c∈ΣがあってΣ⊢¬cとなるのかどうかはあやしい。反例がありそう。だとすれば、この方法はだめだろう。
方法2 Σの述語記号すべてについて+/-のリテラル(Lとする)を作り、Σ⊢Lをさがす。
Pred(Σ)で、Σに含まれるリテラルの述語記号の集合を表すとする。
n引数の述語記号Pについて、n個の変数(x1,x2,...,xn)を用意し
P(x1,x2,...,xn)に符号(+/-)をつけたものを、自由なリテラルと呼ぶことにする。
Σ⊢□が存在するということは、その最後のステップで、どれかの述語記号の自由なリテラル(+と-)の両方が証明できているということである。
だから、
p ∈ Pred(Σ)について、Σからpの自由なリテラル+P(...)と-P(...)の証明が存在するかチェックする。つまり、
Σ⊢+P(...)
Σ⊢-P(...)
をチェックし、両方が証明できればΣは矛盾していることになる。
Σからのすべてのresolventは無限に存在しうるが、自由なリテラルは有限個である。
・補足1
□⊢C の証明が存在しない例
+P, -P, -R⊢□
という証明は存在して、+P -P ⊢ □がそれだが、その証明を変形しても
+P, -P ⊢ +R
は作れない。
・補足2
Σ={□, A}を考える。
論理的にはΣ⊢□だが、resolutionによってΣから□は導出できない。
また、Σ⊢Aもできないので、Σ⊢¬Aの証明も構成できない。