にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Isabell

定理証明器Isabelleで計算可能性の証明

偶然見つけました。 http://www2.score.cs.tsukuba.ac.jp/4eba3005-1/student/takuya-fujiwara-1/cs30bb30df30ca30fc767a88688cc76599-1/CSseminor2008_Fujiwara_Slides.pdf将来、定理証明器で言語の開発をするようになるのかもしれない。チューリング完全性…