セミナーの内容

定理証明支援ツール Isabelle のチュートリアルです．数学や計算機科学の教科書に出てくる証明を確かめたり，プログラムの正しさを証明したりできるようになることを目指します．

第2回のテーマは型と関数の定義・数学的帰納法です。今回までのところで，関数型プログラムの性質を証明できるようになります．特に再帰的に定義された関数の性質を数学的帰納法を用いて証明できるようになります．

プログラム

• Isabelle の基本的な型：論理型，自然数，整数，関数，直積，集合，リスト
• 定数定義 definition
• 代数的データ型定義 datatype
• 関数の再帰的定義 fun
• メソッド: unfold, subst, auto, simp, clarify, arith, induct_tac
• Sledgehammer
• 数学的帰納法
• 演習：関数定義（関数型プログラミング）を行い，その性質を数学的帰納法を用いて示します．

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

セミナー参加の前提条件

前提知識

• Isabelleチュートリアル 第1回程度の Isabelle についての知識
• 代数的データ型：リスト，木
• 関数の再帰的定義（関数型プログラミング）
• 数学的帰納法（高校で習う程度）

必要なもの

• PC
• Isabelle

配布物と Zoom meeting URL

セミナー開始時刻までに CONNPASS のメッセージにてお知らせします。 同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

注意事項

• 配布スライド資料と理論ファイルの公開は禁止です。
• 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
• 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。