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

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

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

May

11

Isar チュートリアル / 定理証明支援系 Isabelle

Organizing : 株式会社 PRINCIPIA

Isar チュートリアル / 定理証明支援系 Isabelle
Hashtag :#Isabelle
Registration info

一般

3000 (Pre-pay)

FCFS
5/10

Attendees
TakeshiHori
sawaragikun
negi23
nsyee
TakayukiTakeuchi
View Attendee List
Start Date
2024/05/11(Sat) 13:00 ~ 18:00
Registration Period

2024/04/13(Sat) 00:00 〜
2024/05/11(Sat) 13:00まで

Location

Zoom

オンライン

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

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

Description

セミナーの内容

定理証明支援ツール Isabelle では、証明を記述する方法が2つあります。1つは apply スタイル、もう1つは Isar スタイルと呼ばれているものです。

Isar スタイルは数学のテキストに書かれている証明のように読めることが特徴です。apply スタイルで記述された証明は、Isabelle の中でコマンドを実行して途中の状態(残されているサブゴール)確認しながらでなければ読めません。これに対して Isar スタイルでは、ある時点までに得られた補題とこれから証明しようとしている命題を証明中に記述することができるので、テキストとして読むことができます。以下に例を示すので雰囲気を味わってみてください。

apply スタイルで書いた証明:

theorem
  "∀x. P ⟶ Q x ⟹ P ⟶ (∀x. Q x)"
apply(rule impI)
apply(rule allI)
apply(drule_tac x="x" in spec)
apply(drule mp)
apply(assumption)
apply(assumption)
done

Isar スタイルで書いた証明:

theorem
  assumes "∀x. P ⟶ Q x"
  shows "P ⟶ (∀x. Q x)"
proof
  assume "P"
  show "∀x. Q x"
  proof
    fix a
    from assms have "P ⟶ Q a" ..
    from this and ‹P› show "Q a" ..
  qed
qed

解説する内容はすべて Isabelle の公式文書に書いてあることです。つまり読めば得られる知識です。それでも、半日集中して習得できるほうがよいという人のためのチュートリアルです。よかったらどうぞ。

講師について

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

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

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

セミナー参加の前提条件

前提知識

  • apply スタイルの知識(Isabelle チュートリアル第1回と第2回程度の知識)

必要なもの

配布物と 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.

Ended

2024/05/11(Sat)

13:00
18:00

Registration Period
2024/04/13(Sat) 00:00 〜
2024/05/11(Sat) 13:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(5)

TakeshiHori

TakeshiHori

Isar チュートリアル / 定理証明支援系 Isabelle に参加を申し込みました!

sawaragikun

sawaragikun

Isar チュートリアル / 定理証明支援系 Isabelle に参加を申し込みました!

negi23

negi23

Isar チュートリアル / 定理証明支援系 Isabelle に参加を申し込みました!

nsyee

nsyee

Isar チュートリアル / 定理証明支援系 Isabelle に参加を申し込みました!

TakayukiTakeuchi

TakayukiTakeuchi

Isar チュートリアル / 定理証明支援系 Isabelle に参加を申し込みました!

Attendees (5)