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