このアルゴリズムは、アメリカの論理学者 H. Wang(ハオ・ワン)が考えたアルゴリズムで、 専門用語では、ワンのアルゴリズムといい、初期の人工知能の研究の代表的アルゴリズムです。
PCalc の作者は神戸大学大学院の住友亮翼さんです。 PCalcは林晋研究室の証明アニメーションプロジェクトで住友さんが開発している ProofWorks という ソフトを元に作られています。
まずは使ってみましょう。 現在使用できるのは、Windows 95 の Internet Explorer Ver.4.0 専用版です。 Ver.3.0 でも使えないことはありません。バグ情報・更新計画を見てください。
PCalcが起動されると、サンプルとして「論理パズルとパズルの論理」p.28 の「赤い手袋」を少し変えたものが入っています。
ただし、現在のバージョンは、まだバグが多いので、命題記号も、 論理記号も、すべて、半角で入力する方が無難です。
論理記号は、IME やATOK の記号入力を使って入力しても同じことです。 もちろん、別な場所に書いておいて、カットアンドペーストしてもかまいません。
「論理パズルとパズルの論理」から例をいくつか書いておきます。 試してみてください。
お母さんは、
雨が降ってる ⇒ 早く帰えるといっているので、これを仮定にします。 ただし、
雨が降ってる 早く帰えるが命題記号ですから、これを定義の欄に入力しておきます。
この仮定は、
雨が降ってる ならば 早く帰えると書いても同じです。ただし、"ならば"の両側の空白は忘れずに入れましょう。
これを聞いて、お父さんは、
¬ 雨が降ってる ⇒ ¬ 早く帰えるといったのです。こちらが結論です。これも、
雨が降ってる でない ならば 早く帰える でないと書けます。
さあ,PCalc は、お父さんの屁理屈に勝てるでしょうか?
(*)賢い ならば 健康である
ということです。さて,下記の(l),(2),(3)のうち,(*) から導かれるのはどれでしょうか?(これらはすべて猫についての命題です。)
(1)(健康である でない) または 賢い (2)健康である または (賢い でない) (3)賢い または 健康である
また、左上のボタンの load, save は、登録したり、読み込んだりのためですが、 今のバージョンでは使えません。clear は今のバージョンでも使えます。