セミナーの内容

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

第1回は論理がテーマです．推論規則を使って命題を証明できるようになることがゴールです．数理論理学の基礎を理解するために，あえて自動証明機能を使わずに推論規則をひとつひとつ使って証明します．この技術は自動ではできない大きな証明を書くときに必要になります．

率直にいって文書を読んで自力で使えるようになる人は参加する必要はありません．しかし新しいツールの使い方を学ぶのはそれなりに苦労があります．定理証明支援ツールのように複雑なツールではなおさらです．大量の文書を読まなければなりません．うまく動かないときには何が悪いのかわかりません．些細なことで多くの時間を失います．使い方に慣れた人に手ほどきを受けた方が効率よく学ぶことができます．疑問があれば質問できます．自分で調べて解決するのはたいへんです．そう考える人に参加してもらえればいいと思います．

シリーズ構成

• 第1回 論理
• 第2回 型と関数の定義・数学的帰納法
• 第3回 集合・関数・関係
• 第4回 集合の帰納的定義

第1回プログラム

1. Isabelle の使い方

• 理論ファイルの構成
• 構文
• メソッド
• 定理

2. 演習

論理学の各演算子について例題を使って定理と使い方の解説を行います．そのあと練習問題をやっていただきます．

3. チャレンジ問題と質疑応答

残りの時間はチャレンジ問題と質疑応答にあてます． 問題を解きたい人は問題をやってください．質問がある人は質問してください． あとで受ける人のために答えを公表することも避けてください．これはお願いです．

講師について

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

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

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

セミナー参加の前提条件

前提知識

数学の授業で習った「～かつ～」，「～または～」，「～でない」，「～ならば～」を知っていればなんとかなると思います．「すべての～について～」と「ある～が存在して～」についてはかんたんに説明します．

必要なもの

• PC
• Isabelle 2020

配布物と Zoom Meeting の URL

セミナー開始時刻までに CONNPASS のメッセージにてお知らせします。 同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

注意事項

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

連絡先

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