お知らせ【メンテナンスのお知らせ】4月25日(木)10:00から1時間半ほど、メンテナンス作業を予定しております。作業の間はconnpassのご利用が出来ません。ご迷惑をおかけしますが何卒ご了承ください。

お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
2024年5月23日(木)以降より開始予定の「connpass 有料API」の料金プランにつきましてはこちらをご覧ください。
なお有料の対象となるのはAPIのみであり、connpassのサービスにつきましては今後も無料でご利用いただけます。

5月

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

主催 : 株式会社 PRINCIPIA

ハッシュタグ：#Isabelle

募集内容	一般 3000円（前払い）先着順 8/10人
申込者	申込者一覧を見る
開催日時	2020/05/24(日) 14:00 ～ 18:00 Googleカレンダー icsファイル
募集期間	2020/05/11(月) 06:47 〜 2020/05/24(日) 13:00まで
会場	Zoom オンライン
前払いについて	前払いについての連絡先: (参加者にのみ公開されます)
	キャンセル・参加費用の払い戻しについて主催者からの説明: お支払いいただくのは資料（スライド資料と理論ファイル）の代金です．セミナー参加費は無料です．したがいまして資料配布後にキャンセルしても代金は返却されません．特に主催者から見て資料配布後にキャンセルを認識した場合は返却されません．よくご検討の上，お申し込みください．
	領収データの発行: 発行しない (詳しくはこちら)

イベントの説明

セミナーの内容

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

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

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

プログラム

1. Isabelle の使い方

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

2. 演習

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

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

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