新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

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

Jun

7

Isabelleチュートリアル 第3回 集合・関数・関係

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

一般

4000 (Pre-pay)

FCFS
14/15

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

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

Description

お知らせ

6月7日 00:25 頃に資料と Zoom meeting に関するメッセージを CONNPASS から送信しました. 届いていない方がいらっしゃいましたらご連絡ください.

セミナーの内容

定理証明支援ツール Isabelle のチュートリアルです.数学や計算機科学の教科書に出てくる証明を確かめたり,プログラムの正しさを証明したりできるようになることを目指します.

第3回のテーマは集合・関数・関係です.数学の基礎であり,プログラムのモデル化でも重要な役割を果たす集合・関数・関係の表記方法と主要な定理,証明のテクニックを解説します.ここまでの集大成として,計算機科学との関係が深い有名な Knaster–Tarski の不動点定理を証明します.

プログラム

  • 集合・関数・関係の記法
  • 主要な定理と練習問題
  • Knaster–Tarski の不動点定理
  • チャレンジ問題

※ 不動点定理の証明がメインディッシュというわけではなく、逆におまけみたいなものです。大事なことは集合・関数・関係について Isabelle 上で定義や証明が書けるようになることです。その1成果として不動点定理を証明してみようというだけのことです。証明自体も難しくありませんが、定理が成り立つ仕組みはかなり興味深いものです。有名な定理が証明できるというとモチベーションが上がりますよね。

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

セミナー参加の前提条件

前提知識

  • Isabelleチュートリアル 第2回まで程度の Isabelle についての知識
  • 集合・関数・関係の基本的な知識(高校程度+α)

必要なもの

配布物

スライド資料(PDF)と Isabelle の理論ファイルを CONNPASS のメッセージにて配布します。

Zoom Meeting link

CONNPASS のメッセージにてお知らせします。

Slack

https://join.slack.com/t/syncstitch/shared_invite/zt-e52dcyza-Vs0vCglGNcPSGOFriRIehQ

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。
  • 第1回,2回と異なり,13時開始で5時間の予定です.最後の方は演習時間になります(退出はご自由にどうぞ).

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。

Media View all Media

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

Ended

2020/06/07(Sun)

13:00
18:00

Registration Period
2020/05/20(Wed) 00:00 〜
2020/06/07(Sun) 12:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(14)

niszet

niszet

Isabelleチュートリアル 第3回 集合・関数・関係 に参加を申し込みました!

tkokamo

tkokamo

Isabelleチュートリアル 第3回 集合・関数・関係に参加を申し込みました!

TakeshiHori

TakeshiHori

Isabelleチュートリアル 第3回 集合・関数・関係 に参加を申し込みました!

murakami_motokazu_1213

murakami_motokazu_1213

Isabelleチュートリアル 第3回 集合・関数・関係に参加を申し込みました!

elkel53930

elkel53930

Isabelleチュートリアル 第3回 集合・関数・関係に参加を申し込みました!

Kuniwak

Kuniwak

Isabelleチュートリアル 第3回 集合・関数・関係に参加を申し込みました!

tos

tos

Isabelleチュートリアル 第3回 集合・関数・関係 に参加を申し込みました!

kubota_junshi

kubota_junshi

I joined Isabelleチュートリアル 第3回 集合・関数・関係!

リチャード伊真岡

リチャード伊真岡

Isabelleチュートリアル 第3回 集合・関数・関係 に参加を申し込みました!

shigemi1014

shigemi1014

I joined Isabelleチュートリアル 第3回 集合・関数・関係!

Attendees (14)