セミナーの内容

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

第4回のテーマは集合の帰納的定義です．数学や計算機科学では帰納的定義が頻繁に使われます．例えば次のようなものです：

• 再帰的に定義された関数
• 代数的データ型
• 公理と推論規則による正しい判断の集合（理論）：論理学，操作的意味論，型理論
• 文脈自由文法（あるいは Backus-Naur form, BNF）
• 関係の反射的推移的閉包

Isabelle には集合を帰納的に定義するための専用の機能があり，それを使うと上記のような対象を表現して性質を証明できるようになります．今回はこの機能の使い方を解説します．解説の後は演習問題をやっていただきます．

今回までのところで，公理と推論規則の集まりで定義された理論そのものを対象とする証明を書くことができるようになります．ご自分の興味にしたがって様々な教科書に挑戦できるようになるでしょう．

プログラム

• 集合を帰納的に定義するためのコマンド inductive_set
• Rule induction: 帰納法
• Rule inversion: 余計な要素が入っていないこと
• 事例
• 演習問題
• チャレンジ問題

講師について

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

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

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

セミナー参加の前提条件

前提知識

• Isabelleチュートリアル 第3回まで程度の Isabelle についての知識

必要なもの

• PC
• Isabelle

配布物と Zoom Meeting

イベント申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします．

事前に同じメッセージを複数回送信する場合があります．ご了承ください．

注意事項

• 配布スライド資料と理論ファイルの公開は禁止です。
• 不測の事態によりイベントが開催できなかった場合または中断せざるを得なくなった場合は，再挙行にて対応させていただきます．

連絡先

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