セミナーの内容

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

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

プログラム

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

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

• PC
• Isabelle 2020

配布物

スライド資料（PDF)と Isabelle の理論ファイルを CONNPASS のメッセージにて配布します。

Zoom Meeting link

CONNPASS のメッセージにてお知らせします。

Slack

https://join.slack.com/t/syncstitch/shared_invite/zt-e52dcyza-Vs0vCglGNcPSGOFriRIehQ

注意事項

• 配布スライド資料と理論ファイルの公開は禁止です。

連絡先

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