版元ドットコム

探せる、使える、本の情報

文芸 新書 社会一般 資格・試験 ビジネス スポーツ・健康 趣味・実用 ゲーム 芸能・タレント テレビ・映画化 芸術 哲学・宗教 歴史・地理 社会科学 教育 自然科学 医学 工業・工学 コンピュータ 語学・辞事典 学参 児童図書 ヤングアダルト 全集 文庫 コミック文庫 コミックス(欠番扱) コミックス(雑誌扱) コミックス(書籍) コミックス(廉価版) ムック 雑誌 増刊 別冊 ラノベ
Coq/SSReflect/MathCompによる定理証明 萩原 学(著/文) - 森北出版
..
詳細画像 0 詳細画像 1 詳細画像 2

書店員向け情報 HELP

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

自然科学
このエントリーをはてなブックマークに追加
発行:森北出版
菊判
224ページ
定価 3,200円+税
ISBN
978-4-627-06241-2   COPY
ISBN 13
9784627062412   COPY
ISBN 10h
4-627-06241-9   COPY
ISBN 10
4627062419   COPY
出版者記号
627   COPY
Cコード
C3041  
3:専門 0:単行本 41:数学
出版社在庫情報
不明
書店発売日
登録日
2018年3月2日
最終更新日
2018年3月2日
このエントリーをはてなブックマークに追加

紹介

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

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

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

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

目次

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

著者プロフィール

萩原 学  (ハギワラ マナブ)  (著/文

千葉大学准教授 博士(数理科学)

アフェルト・レナルド  (アフェルト レナルド)  (著/文

産業技術総合研究所主任研究員 博士(情報理工)

上記内容は本書刊行時のものです。