PVSで、サーチしたらここが引っかかったよ。２ｃｈスゲー（笑）

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

てゆーか、証明アルゴリズムって実際resolutionとかtableau method
とかいうのと、あとは述語論理の場合unificationくらいでしょ。

そういえば、最近のPVSはShostak法とかいう不等式決定方法が追加した
みたいね。式の移項程度のレベルだと自動で証明できちゃうみたい。

＃ちなみにPVSは、Allegro LISPでインプリメントされてます。