May

16
Isabelleチュートリアル第1回論理

Organizing : 株式会社 PRINCIPIA

Hashtag ：#Isabelle

Registration info	一般￥3000 (Pre-pay) FCFS 9/15
About Prepayment	About Prepayment Contact Info: (Only shown to attendees.)
	Cancel/Refund Policy: お支払いいただくのは資料（スライド資料と理論ファイル）の代金です．セミナー参加費は無料です．したがいまして資料配布後にキャンセルしても代金は返却されません．特に主催者から見て資料配布後にキャンセルを認識した場合は返却されません．よくご検討の上，お申し込みください．
	Print receipt data: 発行しない (詳しくはこちら)

Description

セミナーの内容

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

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

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

プログラム

1. Isabelle の使い方

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

2. 演習

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

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

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