お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
2024年5月23日(木)以降より開始予定の「connpass 有料API」の料金プランにつきましてはこちらをご覧ください。

お知らせ connpassをご利用いただく全ユーザーにおいて健全で円滑なイベントの開催や参加いただけるよう、イベント参加者向け・イベント管理者向けのガイドラインページを公開しました。内容をご理解の上、イベント内での違反行為に対応する参考としていただきますようお願いいたします。

このエントリーをはてなブックマークに追加

Mar

18

強い数学的帰納法のひみつ

強い数学的帰納法にある"あれ"の謎に迫る

Organizing : PRINCIPIA Limited

強い数学的帰納法のひみつ
Registration info

参加枠

Free

Attendees
1

Attendees
gaxiiiiiiiiiiii
View Attendee List
Start Date
2023/03/18(Sat) 16:00 ~ 17:30
Registration Period

2023/03/18(Sat) 00:00 〜
16:00まで

Location

Zoom

オンライン

参加者への情報
(参加者と発表者のみに公開されます)

Description

定理証明支援系 Isabelle/HOL や Coq で、帰納的に集合や述語を定義すると、数学的帰納法の規則が生成されます。

たとえば Isabelle/HOL で偶数の集合を帰納的に定義すると、こんな感じです:

inductive_set E where
  base: "0 ∈ E"
| step: "n ∈ E ⟹ Suc (Suc n) ∈ E"

thm E.induct
  ?x  E; ?P 0; n. n  E; ?P n  ?P (Suc (Suc n))  ?P ?x

帰納法の仮定をみると、ふつうの P n に加えて n ∈ E というものがあります。これははなんでしょう?

帰納法の仮定に条件が追加されているわけですから、仮定が強くなっているということです。つまり、証明しやすくなっているわけです。どうしてこのようなことができるのでしょうか。

このような強い数学的帰納法がなりたつことの証明を追ってみたいと思います。証明を追っていくのでなかなかたいへんですが、興味があればどうぞ。

Isabelle/HOL の知識を前提とします。

Media View all Media

If you add event media, up to 3 items will be shown here.

Feed

hatsugai

hatsugai published 強い数学的帰納法のひみつ.

03/17/2023 23:59

Ended

2023/03/18(Sat)

16:00
17:30

Registration Period
2023/03/18(Sat) 00:00 〜
16:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(1)

gaxiiiiiiiiiiii

gaxiiiiiiiiiiii

強い数学的帰納法のひみつ に参加を申し込みました!

Attendees (1)