Coq/SSReflect/MathCompによる定理証明

フリーソフトではじめる数学の形式化

千葉大学准教授 博士(数理科学) 萩原学 (共著) 産業技術総合研究所主任研究員 博士(情報理工) アフェルト・レナルド (共著)

コンピュータと協働して数学する!
定理証明支援系Coq/SSReflect/MathComp,待望の入門書.

◆定理証明支援系とは?
数学の定理証明を支援するソフトウェアのこと.数学の高度化に伴い,従来の「紙と鉛筆」では証明の構成・検証がますます困難になるなか,Coqをはじめとする定理証明支援系が開発されてきました.こうしたシステムには,証明の正しさを保証する機能のほか,証明をコンピュータが扱える形に翻訳する「数学の形式化」の作業を効率化する仕組みが備えられています.実際Coqは「四色定理」や「ケプラー予想」といった歴史的な大問題を解くのにも利用され,話題をよびました.

◆日本語初のチュートリアル
本書は,Coqとその拡張言語SSReflect/MathCompの初となる解説書です.定理証明支援系の研究利用と普及を手がけてきた著者らが,開発環境のインストール手順から基本的な操作,代表的な命令・ライブラリの使い方までを案内します.集合論,代数学,確率・統計,そして情報理論の簡単な定理を題材に,Coq/SSReflect/MathCompの使い方を易しく例示.本書をひととおり読みこなせば,幅広い分野の定理を形式化する力が自然と身につくはずです.

◆まずは触ってみよう!
数学者を目指す方は「大規模証明時代の必須ツール」として,プログラマの方であれば「ソフトウェア検証などの応用を見据えた基礎トレーニング」として,Coq/SSReflect/MathCompに触れてみてはいかがでしょうか.コンピュータと手を携えて定理をつくっていく――その新感覚の面白さに,きっと魅了されることでしょう.

¥3,456

  • 224ページ
  • 978-4-627-06241-2
  • 2018.04
  • 弊社Webサイトのウィンドウ(タブ)を閉じると、カートの内容は消去されます。
  • 送料は無料です。代金引換の手数料は定価の合計金額が10,800円未満の場合 324円(税込)、それ以上の場合は無料です。
  • 一部の離島では代金引換を利用できません。
  • 詳しいご利用方法

現在のカート内容

冊数はご購入確認時に指定できます。

選択した書籍をカートに入れます。
宜しければ「カートに入れる」を押してください。