タブローを描くプログラム

タブローを描くプログラム

http://www.at-akada.org/works/tableau/

手がかかったわりに、まったく一般性が無いネタですが、タブローを描くプログラムをつくりました。

これでもう、「あれ？ この式って恒真かな？ 矛盾式かな？」という理由で悩まなくてもすみますね！

■ タブローについて

タブローというのは、論理式 (の集合) が矛盾しているかどうかを確かめる手法の1つです。

大まかに言うと、タブローは論理式を見ながらルールに従って図を描くという手法です。論理式 (の集合) が矛盾していた場合、タブローは閉じたタブローになります。これによって矛盾した式であるかどうかを判定できます。一方恒真式 (絶対正しい式) の否定は矛盾した式になるので、これを利用して恒真式 (トートロジー) であるかどうかも判定できます。

タブローについて、詳しくは以下の本などに載っています。

(わたしは論理学をつくるしか読んでないけど)。

• 『論理学をつくる』

• 『形式論理学―その展望と限界』

• 『タブローの方法による論理学入門』

ちゃんと説明する自身は無いですが、一応簡単にルールの説明も。

• 「AかつB」があればAとBを縦に並べる
• 縦に並べたなかにPとPの否定があれば、矛盾しているので×をつける
• 「AまたはB」があれば経路を分岐させ、Aが正しい場合とBが正しい場合に分ける
• 2つに分けた経路の両方に×がつくならば、矛盾している
• 「否定」、「または」、「かつ」以外の演算子は「否定」、「または」、「かつ」を使って書き直す

大まかに言うと、タブローはこういう方法です。この説明じゃ絶対にわからないと思いますが、これ以上口で説明するのはわたしには無理なので詳しく知りたい場合は上の本などを読んで下さい。

ちなみに命題論理にしか対応してません。

■ 描いてみた感想

やりたかったのは、

• JavaScriptで論理式の構文解析
• HTMLでちょっとずつタブローを描く

の2つなので、わたしは大体満足しました。完全な自己満足プログラムです。

パーサ部分などは、以下の記事などを参考にしました。

• お手軽パーザー

タブローはHTML + CSS で無理して描いているのですが、IEの表示がさっぱり直らなくて泣きました。いまだにIEでの表示はちょっとおかしいですが、もういいです。IEをつかってるやつを一人一人つかまえて止めるように説得したい気分です。なるべくFirefoxかOperaで見てください。

(Safariはwindows版しか見てないが一応動くらしい)。

■ 使い方の例

あとは適当に使い方の例を示してみます。

以下は『論理学をつくる』のp100にあった練習問題です。

次の4つのことを同時に信じている人がいる。その人の信念は矛盾しているかそれとも整合的か。

• 神は存在する
• 神が存在するならば神が造り給いしこの世は最善の世界である
• 神が造り給いしこの世が最善の世界であるならば悪はこの世にない
• この世には悪がある

E: 神が存在する

W: 神が造り給いしこの世は最善の世界である

B: この世には悪がある

と置くと、題意の命題はそれぞれ

E
E⊃W
W⊃￢B
B

となる。あとはこの4式からタブローを描いてみて、矛盾しているかどうかをチェックすればよい。

↓結果。

http://www.at-akada.org/works/tableau/?E%0AE%E2%8A%83W%0AW%E2%8A%83%EF%BF%A2B%0AB

また、A,B,Cなどの前提からDを導く論証が適切であった場合、集合「A,B,C,￢D」は全体として矛盾する。

(A,B,Cの前提の下でさらに￢Dを認めると、矛盾する。だから前提A,B,Cを認めるなら必ずDも認めなきゃならねえんだよ！ということ)。

つまりタブローをうまく使えば論証が適切であるかどうかも確かめられるので、お、これは便利！かもしれない。

■ ソース

http://www.at-akada.org/download/tableau.zip

オープンソースです。

(大部分JavaScriptなので元々オープンだが)。

index.cgiはrubyが動く環境で動く。

ただしindex.cgiは単に式をURLでわたせるようにしただけなので通常はindex.htmlをブラウザで開くだけで十分だと思われる。