検索条件

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

タグ一覧

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 チュートリアル 第3回 集合・関数・関係

  • 数学
2024/05/05(日)
12:00〜18:00

主催:PRINCIPIA

セミナーの内容

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

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

プログラム

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

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

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

配布物と Zoom meetin URL

CONNPASS のメッセージにて配布します。

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。
  • 第1,2回と異なり,12時開始で6時間の予定です.

連絡先

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