BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:強い数学的帰納法のひみつ
X-WR-CALNAME:強い数学的帰納法のひみつ
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:896632@techplay.jp
SUMMARY:強い数学的帰納法のひみつ
DTSTART;TZID=Asia/Tokyo:20230318T160000
DTEND;TZID=Asia/Tokyo:20230318T173000
DTSTAMP:20260409T162406Z
CREATED:20230317T213257Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/89663
 2?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n定理証明支
 援系 Isabelle/HOL や Coq で、帰納的に集合や述語を定義す
 ると、数学的帰納法の規則が生成されます。\nたとえ
 ば Isabelle/HOL で偶数の集合を帰納的に定義すると、こ
 んな感じです：\ninductive_set E where\n  base: "0 ∈ E"\n| step: 
 "n ∈ E ⟹ Suc (Suc n) ∈ E"\n\nthm E.induct\n  ⟦?x ∈ E\; ?P 0\; 
 ⋀n. ⟦n ∈ E\; ?P n⟧ ⟹ ?P (Suc (Suc n))⟧ ⟹ ?P ?x\n\n\n帰納
 法の仮定をみると、ふつうの P n に加えて n ∈ E とい
 うものがあります。これははなんでしょう？\n帰納法
 の仮定に条件が追加されているわけですから、仮定が
 強くなっているということです。つまり、証明しやす
 くなっているわけです。どうしてこのようなことがで
 きるのでしょうか。\nこのような強い数学的帰納法が
 なりたつことの証明を追ってみたいと思います。証明
 を追っていくのでなかなかたいへんですが、興味があ
 ればどうぞ。\nIsabelle/HOL の知識を前提とします。
LOCATION:Zoom オンライン
URL:https://techplay.jp/event/896632?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR