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

• 資料種別: 図書
• ISBN: 978-4-627-06241-2
• タイトル: Coq/SSReflect/MathCompによる定理証明 : フリーソフトではじめる数学の形式化
• タイトルよみ: コック エスエスリフレクト マス コンプ ニ ヨル テイリ ショウメイ : フリー ソフト デ ハジメル スウガク ノ ケイシキカ
• 著者・編者: 萩原学, アフェルト・レナルド 共著
• 著者標目: 萩原, 学, 1974- ハギワラ, マナブ, 1974- ( 001117071 )典拠; Affeldt, Reynald, 1976- ( 001292493 )典拠
• 出版事項: 東京 : 森北出版
• 出版年月日等: 2018.4
• 出版年（W3CDTF）: 2018
• 数量: 211p
• 大きさ: 22cm
• 出版地（国名コード）: JP
• 本文の言語コード: jpn
• 件名標目: 記号論理学 キゴウロンリガク ( 00565709 )典拠
• NDC10版: 410.96 : 数学
• NDLC: MA41
• 対象利用者: 一般
• 書誌注記: 索引あり
• 入手条件・定価: 3200円
• 所蔵機関: 国立国会図書館
• 請求記号: MA41-L81
• 連携機関・データベース: 国立国会図書館 : 国立国会図書館蔵書; https://ndlsearch.ndl.go.jp
• 書誌ID（NDLBibID）: 028927081; http://id.ndl.go.jp/bib/028927081
• 全国書誌番号: 23055195
• トーハンMARC番号: 33754326
• 目録規則: 日本目録規則1987年版改訂版
• 整理区分コード: 111

• 要約等: コンピュータと協働して数学する！定理証明支援系Coq/SSReflect/MathComp，待望の入門書．（提供元: 出版情報登録センター（JPRO））
• 著者紹介: 萩原 学 千葉大学准教授 博士（数理科学）アフェルト・レナルド 産業技術総合研究所主任研究員 博士（情報理工）（提供元: 出版情報登録センター（JPRO））

目次

第1章　Coq/SSReflect/MathCompとは

第2章　使ってみよう

第3章　命令

第4章　MathCompライブラリの基本ファイル

第5章　集合の形式化