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

Jul

12

帰納的に定義された集合と最小不動点の密な関係

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

一般

1000 (Pre-pay)

FCFS
2/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.CONNPASS上でキャンセルしても,セミナー当日に不参加であったとしても参加費用は返却されません.

Print receipt data:

発行しない (詳しくはこちら)

Description

帰納的に定義された集合と最小不動点の密な関係

Isabelle チュートリアル第3回で,単調な関数は不動点を持つという Knaster–Tarski の定理(の集合限定版)を証明しました.また第4回では集合を帰納的に定義する方法 inductive_set を解説しました.

この2つには密接な関係があります.それについて解説します.この関係を理解すると,帰納的に定義された集合に関する証明の方針を立てる力がつきます.

今回は Isabelle 上での解説のみとなります.スライド資料はありません.

理論ファイルは CONNPASS のメッセージにて配布します.

Isabelle チュートリアル第1回~第4回の知識を前提とします.

Media View all Media

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

Group

PRINCIPIA

Number of events 82

Members 226

Ended

2020/07/12(Sun)

16:00
17:00

Registration Period
2020/07/12(Sun) 00:00 〜
15:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(2)

niszet

niszet

帰納的に定義された集合と最小不動点の密な関係 に参加を申し込みました!

Kuniwak

Kuniwak

帰納的に定義された集合と最小不動点の密な関係に参加を申し込みました!

Attendees (2)