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

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

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

Jun

14

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

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:

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

Print receipt data:

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

Description

セミナーの内容

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

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

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

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

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

プログラム

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

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

配布物

スライド資料(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.

Ended

2020/06/14(Sun)

14:00
18:00

Registration Period
2020/05/28(Thu) 00:00 〜
2020/06/14(Sun) 13:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(9)

tkokamo

tkokamo

Isabelleチュートリアル 第4回 集合の帰納的定義に参加を申し込みました!

Kuniwak

Kuniwak

Isabelleチュートリアル 第4回 集合の帰納的定義に参加を申し込みました!

elkel53930

elkel53930

Isabelleチュートリアル 第4回 集合の帰納的定義に参加を申し込みました!

TakeshiHori

TakeshiHori

Isabelleチュートリアル 第4回 集合の帰納的定義 に参加を申し込みました!

niszet

niszet

Isabelleチュートリアル 第4回 集合の帰納的定義 に参加を申し込みました!

tos

tos

Isabelleチュートリアル 第4回 集合の帰納的定義 に参加を申し込みました!

tukejonny

tukejonny

Isabelleチュートリアル 第4回 集合の帰納的定義 に参加を申し込みました!

Ken Sonoda

Ken Sonoda

Isabelleチュートリアル 第4回 集合の帰納的定義に参加を申し込みました!

shigemi1014

shigemi1014

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

Attendees (9)