BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:Isabelle チュートリアル 第2回 型と関数の定義
 ・数学的帰納法
X-WR-CALNAME:Isabelle チュートリアル 第2回 型と関数の定義
 ・数学的帰納法
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:815775@techplay.jp
SUMMARY:Isabelle チュートリアル 第2回 型と関数の定義・数
 学的帰納法
DTSTART;TZID=Asia/Tokyo:20210503T130000
DTEND;TZID=Asia/Tokyo:20210503T170000
DTSTAMP:20260420T055949Z
CREATED:20210423T142223Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/81577
 5?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n※ connpass か
 らお申し込みができない場合、isaac@principia-m.com までご
 連絡ください。\nセミナーの内容\n定理証明支援ツール
  Isabelle のチュートリアルです．数学や計算機科学の教
 科書に出てくる証明を確かめたり，プログラムの正し
 さを証明したりできるようになることを目指します．\
 n第2回のテーマは型と関数の定義・数学的帰納法です
 。今回までのところで，関数型プログラムの性質を証
 明できるようになります．特に再帰的に定義された関
 数の性質を数学的帰納法を用いて証明できるようにな
 ります．\nプログラム\n\nIsabelle の基本的な型：論理型
 ，自然数，整数，関数，直積，集合，リスト\n定数定
 義 definition\n代数的データ型定義 datatype\n関数の再帰的
 定義 fun\nメソッド: unfold\, subst\, auto\, simp\, clarify\, arith\
 , induct_tac\nSledgehammer\n数学的帰納法\n演習：関数定義（
 関数型プログラミング）を行い，その性質を数学的帰
 納法を用いて示します．\n\n講師について\n株式会社 PRI
 NCIPIA 代表取締役 初谷 久史\nCSP 理論に基づいたモデリ
 ング・検査ツール SyncStitch 開発者\n国立情報学研究所
 トップエスイープロジェクト「並行システムの設計検
 証」講師\nセミナー参加の前提条件\n前提知識\n\nIsabelle
 チュートリアル 第1回程度の Isabelle についての知識\n
 代数的データ型：リスト，木\n関数の再帰的定義（関
 数型プログラミング）\n数学的帰納法（高校で習う程
 度）\n\n必要なもの\n\nPC\nIsabelle\n\n配布物と Zoom meeting UR
 L\nCONNPASS のメッセージにてお知らせします。\n注意事
 項\n\n配布スライド資料と理論ファイルの公開は禁止で
 す。\n\n連絡先\nご質問等がありましたら isaac@principia-m.
 com までお気軽にご連絡ください。
LOCATION:Zoom オンライン
URL:https://techplay.jp/event/815775?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR