Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 [単行本]
    • Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 [単行本]

    • ¥3,520106ポイント(3%還元)
    • 在庫あり2020年12月7日月曜日までヨドバシエクストリームサービス便(無料)がお届け
Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 [単行本]
画像にマウスを合わせると上部に表示
100000009002937220

Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 [単行本]

価格:¥3,520(税込)
ポイント:106ポイント(3%還元)(¥106相当)
お届け日:在庫あり今すぐのご注文で、2020年12月7日月曜日までヨドバシエクストリームサービス便(無料)がお届けします。届け先変更]詳しくはこちら
出版社:森北出版
販売開始日: 2018/04/18
お取り扱い: のお取り扱い商品です。
ご確認事項:返品不可

カテゴリランキング

店舗受け取りが可能です
NEWマルチメディアAkibaマルチメディア梅田マルチメディア博多にて24時間営業時間外でもお受け取りいただけるようになりました

Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 の 商品概要

  • 要旨(「BOOK」データベースより)

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

    第1章 Coq/SSReflect/MathCompとは
    第2章 使ってみよう
    第3章 命令
    第4章 MathCompライブラリの基本ファイル
    第5章 集合の形式化
    第6章 代数学の形式化
    第7章 確率論と情報理論の形式化
  • 内容紹介

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

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

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

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

    萩原 学(ハギワラ マナブ)
    1974年、栃木県足利市生まれ。栃木県立足利高校、千葉大学理学部数学科を経て、2002年、東京大学大学院数理科学研究科博士課程修了。博士(数理科学)。東京大学生産技術研究所(2002年~)を経て、独立行政法人産業技術総合研究所(2005年~)の在職時に、中央大学研究開発機構にて機構准教授(2008/4~2012/3)、ハワイ大学にてResearch Scholar(2011/3~2012/2)などを兼任。2013年より千葉大学准教授。専門は符号理論とそれにかかわる離散数学、組合せ論など

    レナルド,アフェルト(レナルド,アフェルト/Reynald,Affeldt)
    1976年、パ=ド=カレー県ランス市(フランス)生まれ。2000年、ナンシー国立高等鉱業学校Ing´enieur Civil des Mines課程修了。2004年、東京大学大学院情報理工学系研究科博士課程修了。博士(情報理工)。東京大学大学院情報理工学系研究科研究員を経て、2005年より国立研究開発法人産業技術総合研究所、主任研究員
  • 著者について

    萩原 学 (ハギワラ マナブ)
    千葉大学准教授 博士(数理科学)

    アフェルト・レナルド (アフェルト レナルド)
    産業技術総合研究所主任研究員 博士(情報理工)

Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 の商品スペック

商品仕様
出版社名:森北出版
著者名:萩原 学(共著)/アフェルト レナルド(共著)
発行年月日:2018/04/13
ISBN-10:4627062419
ISBN-13:9784627062412
判型:A5
対象:専門
発行形態:単行本
内容:数学
言語:日本語
ページ数:211ページ
縦:22cm
他の森北出版の書籍を探す

    森北出版 Coq/SSReflect/MathCompによる定理証明―フリーソフトではじめる数学の形式化 [単行本] に関するレビューとQ&A

    商品に関するご意見やご感想、購入者への質問をお待ちしています!