いざべる!!
定理証明系(関数型言語でプログラムを書くと、そのプログラムについてなんかの性質を証明できるよ!証明が正しいかどうかはコンピュータがチェックしてくれるよ!証明は大変だけど、多少はコンピュータが手伝ってくれるよ!)だと、国内ではCoqとかAgdaとかが流行ってるみたいですけど、天邪鬼な私はIsabelle/HOLで遊ぶよ!
まずはインストールから。Macだよ。
http://www.cl.cam.ac.uk/research/hvg/Isabelle/
ごちゃごちゃ考えずに、上のサイトからダウンロードするのが良い。Isabelle2009-2とかいうアプリケーションを起動すると、Aquamacsが起動するので、\で円マークが入らないように設定する。elispをコピペしたら、なんかバックスラッシュが\になっちゃったので、適当にぐぐってください。これをやらないと、いろいろ入力できなくて発狂します。
これが一番良い方法かは知りません。でもとりあえず動くよ。こないだつくばに行ったときに先生に聞いてみたら、XでEmacs使ってるとか言ってました。
Aquamacsのメニューから「Proof-General→Options→X-Symbol」にチェック入れておく。これで「\<longrightarrow>」とか書いてスペース押すと→になったりする。
Documentationのページの
- Tutorial on Isabelle/HOL
- Tutorial on Isar
くらいにざっと目を通しておく。正直に言うとあんまり通してません。
日本語の資料だとIsabelle/HOLを用いた定理証明入門というのがある。
で、練習問題はあなぷるを見る。Coqだからちょっと嫌だけど、がんばる。
http://as305.dyndns.org/aps/problem/view/1
lemma "(P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q" proof assume pq: "P \<longrightarrow> Q" from pq have "P \<longrightarrow> Q". qed
多分これで同じ意味になってるんじゃないだろうか。
二番目のFalsoからいきなり難しそうになったので、諦めました。もう寝る時間だしー。
あと全体的にどの記号をどうやって入力するのかがわかりません。困った。