セミナーの内容

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

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

プログラム

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

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

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

• PC
• Isabelle 2020

配布物

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

Zoom Meeting link

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

Slack

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

注意事項

• 配布スライド資料と理論ファイルの公開は禁止です。
• 第1回，2回と異なり，13時開始で5時間の予定です．最後の方は演習時間になります（退出はご自由にどうぞ）．

連絡先

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