Isabelleチュートリアル 第2回 型と関数の定義・数学的帰納法
イベント内容
セミナーの内容
定理証明支援ツール Isabelle のチュートリアルです.数学や計算機科学の教科書に出てくる証明を確かめたり,プログラムの正しさを証明したりできるようになることを目指します.
第2回のテーマは型と関数の定義・数学的帰納法です。今回までのところで,関数型プログラムの性質を証明できるようになります.特に再帰的に定義された関数の性質を数学的帰納法を用いて証明できるようになります.
プログラム
- Isabelle の基本的な型:論理型,自然数,整数,関数,直積,集合,リスト
- 定数定義 definition
- 代数的データ型定義 datatype
- 関数の再帰的定義 fun
- メソッド: unfold, subst, auto, simp, clarify, arith, induct_tac
- Sledgehammer
- 数学的帰納法
- 演習:関数定義(関数型プログラミング)を行い,その性質を数学的帰納法を用いて示します.
講師について
株式会社 PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師
セミナー参加の前提条件
前提知識
- Isabelleチュートリアル 第1回程度の Isabelle についての知識
- 代数的データ型:リスト,木
- 関数の再帰的定義(関数型プログラミング)
- 数学的帰納法(高校で習う程度)
必要なもの
配布物
スライド資料(PDF)と Isabelle の理論ファイルを CONNPASS のメッセージにて配布します。
Zoom Meeting link
CONNPASS のメッセージにてお知らせします。
注意事項
- 配布スライド資料と理論ファイルの公開は禁止です。
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。
注意事項
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。
新規会員登録
このイベントに申し込むには会員登録が必要です。
アカウント登録済みの方はログインしてください。
※ ソーシャルアカウントで登録するとログインが簡単に行えます。
※ 連携したソーシャルアカウントは、会員登録完了後にいつでも変更できます。