ところがおいらは定理証明系を作ったことがないのでこっから先はよく知らん。
詳しくはPaulsonのML for the Working Programmerを見ておくれ。最後の章だっ
たかな?

PVSを使ってみた感じでは、実装したい論理の文法を定義したら多分次に証明
系を構成する要素(context, inference rule)を実装していく。んで、ゴール
をinference ruleを使って分解するためのunificationを書く。そしてそういっ
た分解手続きをプログラミングするためのライブラリを整える、つー感じかな?
勝手に妄想してみました。

MLには定理証明を実装するのにあるとうれしい機能が積極的に追加されている。

* そもそも定理証明系にエラーがあっては話しにならない。とりあえず
型エラーだけでも無くそう => MLは強い型付け
* どうも定理証明をやるとき、ひとまとまりの手順(関数)をプログラム内で再利用できれば
うれしいようだ。あるいは関数で表現できるデータ構造があるときれいに書ける
=> MLは高階関数がある
* unificationにこけたときにすぐに抜けれるとうれしい => 例外
* つーか同じ関数を別々の型で定義し直すのはつかれた => 多相的型付け

Metaであることの意味は586,588両方が正しいのではなかろうか。

定理証明系の実装っつーの普通のはプログラミング言語の実装と違う気がする。
ある形式化された論理をさらに計算機の中で形式化(実装)し、その論理の推論
規則に従って証明をする、という人間の営みを忠実に計算機の中で実現する、
というのに近い。

個人的には電卓と似たようなものだと思う。電卓は人間が「1+2+3」を紙で計
算するところをキーをパチパチうちこんで機械に計算させる。そんな感じで、
黒板の前でうんうんうなるかわりに定理証明系に最初にゴールを入れて、あと
は手でゴールを分解して証明していく。メリットは証明手続きを(ちょっとば
かし)自動化できること、あと人間のケアレスミスを排除できることかな? 電
卓でもそうだよね。

また長かった。逝ってきます。