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

お知らせ connpassをご利用いただく全ユーザーにおいて健全で円滑なイベントの開催や参加いただけるよう、イベント参加者向け・イベント管理者向けのガイドラインページを公開しました。内容をご理解の上、イベント内での違反行為に対応する参考としていただきますようお願いいたします。

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

May

6

Isabelle チュートリアル 第4回 集合の帰納的定義

Organizing : 株式会社 PRINCIPIA

Isabelle チュートリアル 第4回 集合の帰納的定義
Hashtag :#Isabelle
Registration info

一般

3000 (Pre-pay)

FCFS
0/10

Start Date
2024/05/06(Mon) 13:00 ~ 17:00
Registration Period

2024/04/03(Wed) 00:00 〜
2024/05/06(Mon) 00:00まで

Location

Zoom

オンライン

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.

Print receipt data:

発行しない (詳しくはこちら)
出席登録
(イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます)

Description

セミナーの内容

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

第4回のテーマは集合の帰納的定義です.数学や計算機科学では帰納的定義が頻繁に使われます.例えば次のようなものです:

  • 再帰的に定義された関数
  • 代数的データ型
  • 公理と推論規則による正しい判断の集合(理論):論理学,操作的意味論,型理論
  • 文脈自由文法(あるいは Backus-Naur form, BNF)
  • 関係の反射的推移的閉包

Isabelle には集合を帰納的に定義するための専用の機能があり,それを使うと上記のような対象を表現して性質を証明できるようになります.今回はこの機能の使い方を解説します.解説の後は演習問題をやっていただきます.

今回までのところで,公理と推論規則の集まりで定義された理論そのものを対象とする証明を書くことができるようになります.ご自分の興味にしたがって様々な教科書に挑戦できるようになるでしょう.

プログラム

  • 集合を帰納的に定義するためのコマンド inductive_set
  • Rule induction: 帰納法
  • Rule inversion: 余計な要素が入っていないこと
  • 事例
  • 演習問題
  • チャレンジ問題

講師について

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

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

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

セミナー参加の前提条件

前提知識

  • Isabelleチュートリアル 第3回まで程度の Isabelle についての知識

必要なもの

配布物と Zoom Meeting

イベント申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします.

事前に同じメッセージを複数回送信する場合があります.ご了承ください.

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。
  • 不測の事態によりイベントが開催できなかった場合または中断せざるを得なくなった場合は,再挙行にて対応させていただきます.

連絡先

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

Media View all Media

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

Feed

hatsugai

hatsugai published Isabelle チュートリアル 第4回 集合の帰納的定義.

04/03/2024 19:00

Isabelle チュートリアル 第4回 集合の帰納的定義 を公開しました!

krxross

krxross wrote a comment.

2021/07/13 10:38

第二回までさんかさせていただいたkrxrossです。第二回がまだ消化できていないので、第三回に参加しませんでしたが、次回は参加したいと思います。第二回がまだわからないという場合はもう一度第二回に参加させていただきたいです。セミナーの需要の関係もあるので1年後になるかもしれませんがよろしくお願いいたします

Group

PRINCIPIA

Number of events 112

Members 249

Public

2024/05/06(Mon)

13:00
17:00

Please login to register

Registration Period
2024/04/03(Wed) 00:00 〜
2024/05/06(Mon) 00:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(0)

No attendees yet.

Attendees (0)