以下はssreflectをMacで動かそうとした悪戦苦闘の記録です。 最終的には、以下のような構成になりました。 Mac OS X 10.9.4 Emacs 24.3.1 ProofGeneral4.2 Coq8.4pl4 ssreflect1.5 CoqIDE or ProofGeneral Mac OS X 10.9では、CoqIDE8.4は起動できません。既…

定理証明支援って何？ 最近、定理証明支援に関連するニュースがいくつか飛び込んできました。あるときはOpenSSLのバグを見つけ、あるときは数学の問題を解決しています。 それらに共通する定理証明支援とは何かを簡単に説明します。定理証明支援の「定理」「…