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

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

May

24

Isabelleチュートリアル 第1回 論理

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

一般

3000 (Pre-pay)

FCFS
8/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お支払いいただくのは資料(スライド資料と理論ファイル)の代金です.セミナー参加費は無料です.したがいまして資料配布後にキャンセルしても代金は返却されません.特に主催者から見て資料配布後にキャンセルを認識した場合は返却されません.よくご検討の上,お申し込みください.

Print receipt data:

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

Description

セミナーの内容

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

チュートリアルはテーマごとに何回かに分けて不定期に開催します.今回は第1回目で,論理がテーマです.推論規則を使って命題を証明できるようになることがゴールです.数理論理学の基礎を理解するために,あえて自動証明機能を使わずに推論規則をひとつひとつ使って証明します.この技術は自動ではできない大きな証明を書くときに必要になります.

率直にいって文書を読んで自力で使えるようになる人は参加する必要はありません.しかし新しいツールの使い方を学ぶのはそれなりに苦労があります.定理証明支援ツールのように複雑なツールではなおさらです.大量の文書を読まなければなりません.うまく動かないときには何が悪いのかわかりません.些細なことで多くの時間を失います.使い方に慣れた人に手ほどきを受けた方が効率よく学ぶことができます.疑問があれば質問できます.自分で調べて解決するのはたいへんです.そう考える人に参加してもらえればいいと思います.

プログラム

1. Isabelle の使い方

  • 理論ファイルの構成
  • 構文
  • メソッド
  • 定理

2. 演習

論理学の各演算子について例題を使って定理と使い方の解説を行います.そのあと練習問題をやっていただきます.

3. チャレンジ問題と質疑応答

残りの時間はチャレンジ問題と質疑応答にあてます. 問題を解きたい人は問題をやってください.質問がある人は質問してください. 18:00 で終了です.終わらなかった問題は各自やってください.質問はメールで受け付けます. 進捗に応じたヒントは出しますが,答えそのものは教えません. あとで受ける人のために答えを公表することも避けてください.これはお願いです.

講師について

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

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

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

セミナー参加の前提条件

前提知識

数学の授業で習った「~かつ~」,「~または~」,「~でない」,「~ならば~」を知っていればなんとかなると思います.「すべての~について~」と「ある~が存在して~」についてはかんたんに説明します.

必要なもの

配布物

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

Zoom Meeting link

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

Slack

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

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。

連絡先

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

Media View all Media

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

Feed

Ken Sonoda

Ken Sonoda wrote a comment.

2020/05/24 14:00

5分ほど遅れます

Ended

2020/05/24(Sun)

14:00
18:00

Registration Period
2020/05/11(Mon) 06:47 〜
2020/05/24(Sun) 13:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(8)

niszet

niszet

Isabelleチュートリアル 第1回 論理 に参加を申し込みました!

Yusuke Kataoka

Yusuke Kataoka

Isabelleチュートリアル 第1回 論理に参加を申し込みました!

yoshihiro503

yoshihiro503

Isabelleチュートリアル 第1回 論理 に参加を申し込みました!

sasuseso

sasuseso

Isabelleチュートリアル 第1回 論理 に参加を申し込みました!

Ken Sonoda

Ken Sonoda

Isabelleチュートリアル 第1回 論理に参加を申し込みました!

tkob

tkob

Isabelleチュートリアル 第1回 論理 に参加を申し込みました!

antizigzag

antizigzag

Isabelleチュートリアル 第1回 論理 に参加を申し込みました!

リチャード伊真岡

リチャード伊真岡

Isabelleチュートリアル 第1回 論理 に参加を申し込みました!

Attendees (8)