検索条件

キーワード
タグ
ツール
開催日
こだわり条件

タグ一覧

JavaScript
PHP
Java
Ruby
Python
Perl
Scala
Haskell
C言語
C言語系
Google言語
デスクトップアプリ
スマートフォンアプリ
プログラミング言語
U/UX
MySQL
RDB
NoSQL
全文検索エンジン
全文検索
Hadoop
Apache Spark
BigQuery
サーバ構成管理
開発サポートツール
テストツール
開発手法
BI
Deep Learning
自然言語処理
BaaS
PaaS
Iaas
Saas
クラウド
AI
Payment
クラウドソフトウェア
仮想化ソフトウェア
OS
サーバ監視
ネットワーク
WEBサーバ
開発ツール
テキストエディタ
CSS
HTML
WEB知識
CMS
WEBマーケティング
グラフィック
グラフィックツール
Drone
AR
マーケット知識
セキュリティ
Shell
IoT
テスト
Block chain
知識

Isabelle チュートリアル 第4回 集合の帰納的定義

  • 数学
2024/05/06(月)
13:00〜17:00

主催:PRINCIPIA

セミナーの内容

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

第4回のテーマは集合の帰納的定義です.数学や計算機科学では帰納的定義が頻繁に使われます.例えば次のようなものです:

  • 再帰的に定義された関数
  • 代数的データ型
  • 公理と推論規則による正しい判断の集合(理論):論理学,操作的意味論,型理論
  • 文脈自由文法(あるいは Backus-Naur form, BNF)
  • 関係の反射的推移的閉包

Isabelle には集合を帰納的に定義するための専用の機能があり,それを使うと上記のような対象を表現して性質を証明できるようになります.今回はこの機能の使い方を解説します.解説の後は演習問題をやっていただきます.

今回までのところで,公理と推論規則の集まりで定義された理論そのものを対象とする証明を書くことができるようになります.ご自分の興味にしたがって様々な教科書に挑戦できるようになるでしょう.

プログラム

  • 集合を帰納的に定義するためのコマンド inductive_set
  • Rule induction: 帰納法
  • Rule inversion: 余計な要素が入っていないこと
  • 事例
  • 演習問題
  • チャレンジ問題

講師について

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

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

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

セミナー参加の前提条件

前提知識

  • Isabelleチュートリアル 第3回まで程度の Isabelle についての知識

必要なもの

配布物と Zoom Meeting

イベント申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします.

事前に同じメッセージを複数回送信する場合があります.ご了承ください.

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。
  • 不測の事態によりイベントが開催できなかった場合または中断せざるを得なくなった場合は,再挙行にて対応させていただきます.

連絡先

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

Workship