お知らせ 【重要なお知らせ】iOSアプリの運用および提供を2024年6月3日(月)を以て終了いたします。詳細は お知らせをご覧ください。

お知らせ connpassではさらなる価値のあるデータを提供するため、イベントサーチAPIの提供方法の見直しを決定しました。2024年5月23日(木)より 「企業・法人」「コミュニティ及び個人」向けの2プランを提供開始いたします。ご利用にあたっては利用申請及び審査がございます。詳細はヘルプページをご確認ください。

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

May

4

Isabelle チュートリアル 第2回 型と関数の定義・数学的帰納法

Organizing : 株式会社 PRINCIPIA

Isabelle チュートリアル 第2回 型と関数の定義・数学的帰納法
Hashtag :#Isabelle
Registration info

一般

3000 (Pre-pay)

FCFS
2/10

Attendees
negi23
TakayukiTakeuchi
View Attendee List
Start Date
2024/05/04(Sat) 13:00 ~ 17:00
Registration Period

2024/04/03(Wed) 00:00 〜
2024/05/04(Sat) 12:30まで

Location

Zoom

オンライン

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.

Print receipt data:

発行しない (詳しくはこちら)
出席登録
(イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます)

Description

セミナーの内容

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

第2回のテーマは型と関数の定義・数学的帰納法です。今回までのところで,関数型プログラムの性質を証明できるようになります.特に再帰的に定義された関数の性質を数学的帰納法を用いて証明できるようになります.

プログラム

  • Isabelle の基本的な型:論理型,自然数,整数,関数,直積,集合,リスト
  • 定数定義 definition
  • 代数的データ型定義 datatype
  • 関数の再帰的定義 fun
  • メソッド: unfold, subst, auto, simp, clarify, arith, induct_tac
  • Sledgehammer
  • 数学的帰納法
  • 演習:関数定義(関数型プログラミング)を行い,その性質を数学的帰納法を用いて示します.

講師について

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

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

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

セミナー参加の前提条件

前提知識

  • Isabelleチュートリアル 第1回程度の Isabelle についての知識
  • 代数的データ型:リスト,木
  • 関数の再帰的定義(関数型プログラミング)
  • 数学的帰納法(高校で習う程度)

必要なもの

配布物と Zoom meeting URL

セミナー開始時刻までに CONNPASS のメッセージにてお知らせします。 同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。
  • 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
  • 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

連絡先

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

Media View all Media

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

Feed

hatsugai

hatsugai published Isabelle チュートリアル 第2回 型と関数の定義・数学的帰納法.

04/03/2024 19:00

Isabelle チュートリアル 第2回 型と関数の定義・数学的帰納法 を公開しました!

Ended

2024/05/04(Sat)

13:00
17:00

Registration Period
2024/04/03(Wed) 00:00 〜
2024/05/04(Sat) 12:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(2)

negi23

negi23

Isabelle チュートリアル 第2回 型と関数の定義・数学的帰納法 に参加を申し込みました!

TakayukiTakeuchi

TakayukiTakeuchi

Isabelle チュートリアル 第2回 型と関数の定義・数学的帰納法 に参加を申し込みました!

Attendees (2)