ロジックの勉強中３ 命題導出

前回 http://d.hatena.ne.jp/propella/20090717/p1 ブール論理に使う基本的な用語について書いたが、せっかくブール関数計算器 http://languagegame.org/pub/booltable/booltable.html を作ったので、今後記法はそれに合わせてブール関数式にする。目的はある命題がを証明する事。証明とは、あるブール式がいつでも成り立つ(valid である)事を言う。

• 0 : false 偽
• 1 : true 真
• A + B : A or B, A かつ B
• A * B : A and B, A または B
• -A : not A, A では無い
• A => B : A implies B, 含有 A ならば B, B は A を含む

valid と consistent について復習

ブール式は真か偽の値を示す式の事だが、特に変数が含まれる時にある式がの返す値の組み合わせと考える事も出来る。(リンクをクリックすると真理表が出るよ)

• 答えがいつも真の時を valid、答えに偽が含まれる時を invalid と言う。
• 答えに真が含まれる時を consistent、答えがいつも偽の時を inconsistent と言う。

• A+-A は変数がどんな値でも真なので valid で consistent
• A+B は真と偽の両方の可能性があるので invalid で consistent
• A*-A は常に偽なので inconsistent

imply と refutation theorem

論理の性質を現すのに imply がよく使われる。A=>B は、「A の時に B である」の他に、「B が A を含む」と解釈出来る。

A=>B だからといって B=>A とは限らない。A=>B と B=>A の両方が成り立つ時を A=B と書く。次の真理表で確認出来る。

• (A=>B)=(B=>A)
• A=B

A=>B を直接証明しにくい場合に、代わりに A*-B が inconsistent である事を証明しても良い。これを refutation theorem (背理法)という。次の真理表で確かめられる。

• (A=>B)=-(A*-B)

命題導出

次の式

(A+B)*(-B*C)=>(A*C)

を resolution (導出)と言う。この場合変数 B を消去して新しい式を作る。この式と前回書いた CNF を使うと、どんどん変数を消して行ってわりと簡単に証明が出来る。CNF で書くと

• 前提: {{A, B}, {-B, C}}
• 結果: {{A, C}}

となる。これを機械的にやるのはややこしいので、背理法を使う。この場合結果が inconsistent になれば良いので簡単。

• 前提: {{A, B}, {-B, C}}
• 前提: {{A, C}}の否定
• 結果: {} inconsistent

次の真理表で確認。

• (A+B)*(-B+C)*-(A+C)