セミナーの内容

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

チュートリアルはテーマごとに何回かに分けて不定期に開催します．今回は第1回目で，論理がテーマです．推論規則を使って命題を証明できるようになることがゴールです．数理論理学の基礎を理解するために，あえて自動証明機能を使わずに推論規則をひとつひとつ使って証明します．この技術は自動ではできない大きな証明を書くときに必要になります．

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

プログラム

1. Isabelle の使い方

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

2. 演習

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

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

残りの時間はチャレンジ問題と質疑応答にあてます． 問題を解きたい人は問題をやってください．質問がある人は質問してください． 18:00 で終了です．終わらなかった問題は各自やってください．質問はメールで受け付けます． 進捗に応じたヒントは出しますが，答えそのものは教えません． あとで受ける人のために答えを公表することも避けてください．これはお願いです．

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

• PC
• Isabelle 2020

配布物

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

Zoom Meeting link

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

Slack

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

注意事項

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

連絡先

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