BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:Isabelle チュートリアル 第3回 集合・関数・関
 係
X-WR-CALNAME:Isabelle チュートリアル 第3回 集合・関数・関
 係
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:815781@techplay.jp
SUMMARY:Isabelle チュートリアル 第3回 集合・関数・関係
DTSTART;TZID=Asia/Tokyo:20210505T130000
DTEND;TZID=Asia/Tokyo:20210505T180000
DTSTAMP:20260413T124341Z
CREATED:20210423T142258Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/81578
 1?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n※ connpass か
 らお申し込みができない場合、isaac@principia-m.com までご
 連絡ください。\nセミナーの内容\n定理証明支援ツール
  Isabelle のチュートリアルです．数学や計算機科学の教
 科書に出てくる証明を確かめたり，プログラムの正し
 さを証明したりできるようになることを目指します．\
 n第3回のテーマは集合・関数・関係です．数学の基礎
 であり，プログラムのモデル化でも重要な役割を果た
 す集合・関数・関係の表記方法と主要な定理，証明の
 テクニックを解説します．ここまでの集大成として，
 計算機科学との関係が深い有名な Knaster–Tarski の不動
 点定理を証明します．\nプログラム\n\n集合・関数・関
 係の記法\n主要な定理と練習問題\nKnaster–Tarski の不動
 点定理\nチャレンジ問題\n\n※ 不動点定理の証明がメイ
 ンディッシュというわけではなく、逆におまけみたい
 なものです。大事なことは集合・関数・関係について 
 Isabelle 上で定義や証明が書けるようになることです。
 その1成果として不動点定理を証明してみようというだ
 けのことです。証明自体も難しくありませんが、定理
 が成り立つ仕組みはかなり興味深いものです。有名な
 定理が証明できるというとモチベーションが上がりま
 すよね。\n講師について\n株式会社 PRINCIPIA 代表取締役 
 初谷 久史\nCSP 理論に基づいたモデリング・検査ツール
  SyncStitch 開発者\n国立情報学研究所トップエスイープ
 ロジェクト「並行システムの設計検証」講師\nセミナ
 ー参加の前提条件\n前提知識\n\nIsabelleチュートリアル 
 第2回まで程度の Isabelle についての知識\n集合・関数・
 関係の基本的な知識（高校程度＋α）\n\n必要なもの\n\n
 PC\nIsabelle\n\n配布物と Zoom meetin URL\nCONNPASS のメッセージ
 にて配布します。\n注意事項\n\n配布スライド資料と理
 論ファイルの公開は禁止です。\n第1回，2回と異なり，
 13時開始で5時間の予定です．\n\n連絡先\nご質問等があ
 りましたら isaac@principia-m.com までお気軽にご連絡くだ
 さい。
LOCATION:Zoom オンライン
URL:https://techplay.jp/event/815781?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR