関数型言語で定理証明プログラムって書けるんですか？

質問

最近流行っている関数型言語と言うのは、定理証明プログラムを書くことができるのでしょうか？

何年か前に学会誌を取っていたことがあり、その中で ML という関数型言語で定理証明問題を扱っていたような記憶があります。

定理証明問題について勉強するのによい書籍やホームページなどありましたら教えてください。

回答No.1

beforeos · ベストアンサー

ML自体が関数型でそのような目的で付くたれた言語です。
参照USLのPDFがとてもよいと思います。
英語でよければ、処理系は2つほど有名なものがあります。

参考URL：

http://yk.i.hosei.ac.jp/smlbook/smlbook.pdf#search='Meta%20Language'