BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:Isabelle チュートリアル 第4回 集合の帰納的定
 義
X-WR-CALNAME:Isabelle チュートリアル 第4回 集合の帰納的定
 義
X-WR-TIMEZONE:Asia/Tokyo
BEGIN:VTIMEZONE
TZID:Asia/Tokyo
BEGIN:STANDARD
DTSTART:19700101T000000
TZOFFSETFROM:+0900
TZOFFSETTO:+0900
TZNAME:JST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:801537@techplay.jp
SUMMARY:Isabelle チュートリアル 第4回 集合の帰納的定義
DTSTART;TZID=Asia/Tokyo:20201212T130000
DTEND;TZID=Asia/Tokyo:20201212T170000
DTSTAMP:20260502T123331Z
CREATED:20201201T141221Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/80153
 7?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\nセミナーの
 内容\n定理証明支援ツール Isabelle のチュートリアルで
 す．数学や計算機科学の教科書に出てくる証明を確か
 めたり，プログラムの正しさを証明したりできるよう
 になることを目指します．\n第4回のテーマは集合の帰
 納的定義です．数学や計算機科学では帰納的定義が頻
 繁に使われます．例えば次のようなものです：\n\n再帰
 的に定義された関数\n代数的データ型\n公理と推論規則
 による正しい判断の集合（理論）：論理学，操作的意
 味論，型理論\n文脈自由文法（あるいは Backus-Naur form\, 
 BNF）\n関係の反射的推移的閉包\n\nIsabelle には集合を帰
 納的に定義するための専用の機能があり，それを使う
 と上記のような対象を表現して性質を証明できるよう
 になります．今回はこの機能の使い方を解説します．
 解説の後は演習問題をやっていただきます．\n今回ま
 でのところで，公理と推論規則の集まりで定義された
 理論そのものを対象とする証明を書くことができるよ
 うになります．ご自分の興味にしたがって様々な教科
 書に挑戦できるようになるでしょう．\nプログラム\n\n
 集合を帰納的に定義するためのコマンド inductive_set\nRul
 e induction: 帰納法\nRule inversion: 余計な要素が入っていな
 いこと\n事例\n演習問題\nチャレンジ問題\n\n講師につい
 て\n株式会社 PRINCIPIA 代表取締役 初谷 久史\nCSP 理論に
 基づいたモデリング・検査ツール SyncStitch 開発者\n国
 立情報学研究所トップエスイープロジェクト「並行シ
 ステムの設計検証」講師\nセミナー参加の前提条件\n前
 提知識\n\nIsabelleチュートリアル 第3回まで程度の Isabell
 e についての知識\n\n必要なもの\n\nPC\nIsabelle 2020\n\n配布
 物と Zoom Meeting\nイベント申し込み締め切り時刻後に CON
 NPASS のメッセージにてお知らせします．\n事前に同じ
 メッセージを複数回送信する場合があります．ご了承
 ください．\n注意事項\n\n配布スライド資料と理論ファ
 イルの公開は禁止です。\n不測の事態によりイベント
 が開催できなかった場合または中断せざるを得なくな
 った場合は，再挙行にて対応させていただきます．\n\n
 連絡先\nご質問等がありましたら isaac@principia-m.com まで
 お気軽にご連絡ください。
LOCATION:Zoom オンライン
URL:https://techplay.jp/event/801537?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR