| 募集内容 |
一般 1000円（前払い）
先着順
|
|---|---|
| 申込者 |
|
| 開催日時 |
2020/06/17(水) 21:00 ～ 22:30
|
| 募集期間 |
2020/06/17(水) 00:00
〜 |
| 会場 |
Zoom オンライン |
| 前払いについて |
前払いについての連絡先: (参加者にのみ公開されます) |
|
キャンセル・参加費用の払い戻しについて主催者からの説明: お申込み後のキャンセルはできません．セミナーについての説明をよくお読みいただき，十分ご検討の上お申し込みください．CONNPASS上でキャンセルしても，セミナー当日に不参加であったとしても参加費用は返却されません． |
|
|
領収データの発行: 発行しない (詳しくはこちら) |
イベントの説明
セミナーの内容
定理証明支援ツール Isabelle 上でシーケント計算の推論規則を表現し，それを使って証明をします．
自然演繹とはまた違ったパズルを楽しむことができます．
集合の帰納的定義を使って推論規則を表現する典型的な例です．シーケント計算は命題論理の範囲です．
※ カットの話はしません．
プログラム
- シーケント計算
- Isabelle 上での表現
- 証明例
- 演習問題
- チャレンジ問題
講師について
株式会社 PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師
セミナー参加の前提条件
前提知識
- Isabelle の文書 tutorial.pdf の part I, II 程度の知識（Isabelle チュートリアル第1~4回相当）
必要なもの
- 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 までお気軽にご連絡ください。
資料 資料をもっと見る／編集する
資料が投稿されると、最新の3件が表示されます。
フィード
2020/06/17 11:30
hatsugai
エンジニアをつなぐ
connpass は株式会社ビープラウドが開発・運営しています