Coq / Ssreflect / Mathcompによる定理証明 フリーソフトではじめる数学の形式化

「四色定理」や「ケプラー予想」の証明に使われたことでも注目の定理証明支援系。その研究利用と普及を手がけてきた著者らが、開発環境のインストール手順から基本的な操作、代表的な命令・ライブラリの使い方までを丁寧に案内します。

目次 : 第１章　Ｃｏｑ／ＳＳＲｅｆｌｅｃｔ／ＭａｔｈＣｏｍｐとは/ 第２章　使ってみよう/ 第３章　命令/ 第４章　ＭａｔｈＣｏｍｐライブラリの基本ファイル/ 第５章　集合の形式化/ 第６章　代数学の形式化/ 第７章　確率論と情報理論の形式化

【著者紹介】
萩原学 : １９７４年、栃木県足利市生まれ。栃木県立足利高校、千葉大学理学部数学科を経て、２００２年、東京大学大学院数理科学研究科博士課程修了。博士（数理科学）。東京大学生産技術研究所（２００２年〜）を経て、独立行政法人産業技術総合研究所（２００５年〜）の在職時に、中央大学研究開発機構にて機構准教授（２００８／４〜２０１２／３）、ハワイ大学にてＲｅｓｅａｒｃｈ　Ｓｃｈｏｌａｒ（２０１１／３〜２０１２／２）などを兼任。２０１３年より千葉大学准教授。専門は符号理論とそれにかかわる離散数学、組合せ論など

アフェルト・レナルド : １９７６年、パ＝ド＝カレー県ランス市（フランス）生まれ。２０００年、ナンシー国立高等鉱業学校Ｉｎｇ´ｅｎｉｅｕｒ　Ｃｉｖｉｌ　ｄｅｓ　Ｍｉｎｅｓ課程修了。２００４年、東京大学大学院情報理工学系研究科博士課程修了。博士（情報理工）。東京大学大学院情報理工学系研究科研究員を経て、２００５年より国立研究開発法人産業技術総合研究所、主任研究員（本データはこの書籍が刊行された当時に掲載されていたものです）