セミナーの内容

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

第3回のテーマは集合・関数・関係です．数学の基礎であり，プログラムのモデル化でも重要な役割を果たす集合・関数・関係の表記方法と主要な定理，証明のテクニックを解説します．ここまでの集大成として，計算機科学との関係が深い有名な Knaster–Tarski の不動点定理を証明します．

プログラム

• 集合・関数・関係の記法
• 主要な定理と練習問題
• Knaster–Tarski の不動点定理
• チャレンジ問題

※ 不動点定理の証明がメインディッシュというわけではなく、逆におまけみたいなものです。大事なことは集合・関数・関係について Isabelle 上で定義や証明が書けるようになることです。その1成果として不動点定理を証明してみようというだけのことです。証明自体も難しくありませんが、定理が成り立つ仕組みはかなり興味深いものです。有名な定理が証明できるというとモチベーションが上がりますよね。

講師について

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

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

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

セミナー参加の前提条件

前提知識

• Isabelleチュートリアル 第2回まで程度の Isabelle についての知識
• 集合・関数・関係の基本的な知識（高校程度＋α）

必要なもの

• PC
• Isabelle

配布物と Zoom meetin URL

CONNPASS のメッセージにて配布します。

注意事項

• 配布スライド資料と理論ファイルの公開は禁止です。
• 第1，2回と異なり，12時開始で6時間の予定です．

連絡先

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