選言的論理式と場合わけ

同じく、命題論理を例に、場合わけが起こる場合の処理について説明する。 次のMG節集合を考えてみよう。

前節の(1)と違い、(C1')は後件が二つのアトムp,rの選言になっている。

この節集合は、はたして充足不能であろうか、 それとも充足可能でモデルが見つかるであろうか?

1. まず、(C1')により、 無条件に``pが成り立つかqが成り立つ''のだから、 ``pが成り立つ''とするモデルの候補 M1 と、 ``rが成り立つ''とするモデルの候補 M2 を立てることにする。
2. 以下の手続きはモデル候補 M1 と M2 とで、 まったく独立に(順番に、あるいは並行して)進める。
   1. モデル候補 M1 を立てた方では、
      1. pが成り立つとしたから、(C2)によりqが成り立つとする。
      2. qが成り立つとすると、(C3)により矛盾が出る。 結局モデル候補 M1 からはモデルは作れないことが分かる。
   2. モデル候補 M2 を立てた方では、
      1. rが成り立つとしたから、(C4)により矛盾が出る。 結局モデル候補 M2 からもモデルが作れないことが分かる。
3. 結局、M1, M2 のいずれからも矛盾が出てモデルは作れなかった。 すなわち、もともとこの節集合にモデルは作れず、 充足不能であると判定される。

さて、このように節の後件に選言(``または'')が現れるときには、 モデル候補を選言中の各々のアトムで場合分けして 手続きを進めることになる。

場合分けのいずれかでモデルが出来上がる場合には、 もともとの節集合は充足可能で、実際その出来上がったモデルが ひとつのモデルになっている。

さて、今の例から(C4)を取り去って、

としてみよう。 そうすると、MGTP実行では モデル候補 M1 の方はやはりモデルになり得ないが、 モデル候補 M2 の方は矛盾が出ることがなく、 これ以上成り立つべきアトムを要求する非負節もないので、 晴れてモデルとなる。 すなわち、この節集合は充足可能で、 実際 {r} がそのモデルとなっていることがわかる。