新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

このエントリーをはてなブックマークに追加

Jun

17

Isabelle によるシーケント計算

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

一般

1000 (Pre-pay)

FCFS
4/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.CONNPASS上でキャンセルしても,セミナー当日に不参加であったとしても参加費用は返却されません.

Print receipt data:

発行しない (詳しくはこちら)

Description

セミナーの内容

定理証明支援ツール 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 までお気軽にご連絡ください。

Media View all Media

If you add event media, up to 3 items will be shown here.

Feed

Ended

2020/06/17(Wed)

21:00
22:30

Registration Period
2020/06/17(Wed) 00:00 〜
20:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(4)

Kuniwak

Kuniwak

Isabelle によるシーケント計算 に参加を申し込みました!

TakeshiHori

TakeshiHori

Isabelle によるシーケント計算 に参加を申し込みました!

niszet

niszet

Isabelle によるシーケント計算 に参加を申し込みました!

tkokamo

tkokamo

Isabelle によるシーケント計算に参加を申し込みました!

Attendees (4)