conjectureの否定について

[goalについて]

clause集合ΣとclauseCを考える。この文脈で証明したいCのことconjectureと呼ぶ。

Σ⊢Cの証明を作るかわりに、Σ∪{¬C}⊢□の証明が作れたら、Σ⊢Cが証明できると考えるのが反証法である。

証明したい命題Cが存在するので、¬Cを含まないような証明は不要だから、¬Cに着目して証明を構成していく方法は、総当たりで反証を求めるよりも妥当だろう。

この¬Cのことをgoalと呼び、goalから出発して証明を構成していく。この用語は一般的だと思う。

goalのすべてのリテラルを消滅させれば矛盾に辿り着くという考えになる。その消し方にはいろいろな方法があるが、そこには深入りしない。

1. conjectureの否定について

conjectureは、clauseやclauseの集合をとりうるので、それの否定がどういう形になるか考えてみる。

[1clauseの場合]
　- 1リテラルの場合
　　　+Pから-Pを作る
　　　-Pを消去していくことで始まる反証を求めれば良い。

　- 複数リテラルの場合
　　たとえば、clause +P+R-Sを否定すると、clause集合{-P, -R, +S}となる。これはandなので、Σ(もandだから)と和集合にすればよい。
　　この場合、goalは3つになり、この3つのどれかが矛盾する証明を求めればよい。

[複数clauseの場合]
　　goalが、{C1, C2}だとすると、¬g=¬C1∨¬C2となり、Σ∧¬gはそのままではclause集合ではない。そこでΣ∧¬gを標準形に変形すると、ド・モルガンの法則により複数のclauseの集合が発生するが、これも∧-∨の形なので、一つのclause集合Σ'からの反証を求めることになる。ただし、goalの否定が複数のclauseに分散し、元のΣの要素とも合体しているので、goalを消すという目標をどう達成すればよいのか、よくわからない。

例)

例) A,B ⊢((C1∨C2)∧(D1∨D2))
A,BはclauseでC1,C2,D1,D2はリテラルだとする。右辺は2つのclauseになっている。
このとき、conjectureを否定し左辺に追加すると、∧でつなげることになるので、このような論理式から証明を考えることになる。

(A∧B)∧¬((C1∨C2)∧(D1∨D2))

変形していくと。
(A∧B)∧(¬(C1∨C2)∨¬(D1∨D2)
↓
(A∧B)∧((¬C1∧¬C2)∨(¬D1∧¬D2))
↓
(A∧B)∧((¬C1∨¬D1)∧(¬C1∨¬D2)∧(¬C2∨¬D1)∧(¬C2∨¬D2))
↓
{A,B,(¬C1∨¬D1),(¬C1∨¬D2),(¬C2∨¬D1)(¬C2∨¬D2)}

と、1つのclause集合になることはわかる。ここで、goalが何になるかというと(¬C1∨¬D1), (¬C1∨¬D2), (¬C2∨¬D1), (¬C2∨¬D2)の4つのclauseなので、それぞれのclauseをgoalとして4つの証明/反証を見つけ出す手順になる(はず)。
元のconjectureが∨なので、conjectureを構成するすべてのリテラルを消滅させなくてはならないということだろうと思う。(ここは間違っているかもしれない)

こう考えると、clause集合をconjectureとするのはかなり面倒臭い話になる。

たぶん、私はclause集合をconjectureにしようとは思わないので、気にしないのである。