検索条件

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

タグ一覧

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 チュートリアル 第1回 論理

2023/04/02(日)
13:00〜17:00
Googleカレンダーに追加
参加者

1人/10人

主催:PRINCIPIA

セミナーの内容

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

第1回は論理がテーマです.推論規則を使って命題を証明できるようになることがゴールです.数理論理学の基礎を理解するために,あえて自動証明機能を使わずに推論規則をひとつひとつ使って証明します.この技術は自動ではできない大きな証明を書くときに必要になります.

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

シリーズ構成

  • 第1回 論理
  • 第2回 型と関数の定義・数学的帰納法
  • 第3回 集合・関数・関係
  • 第4回 集合の帰納的定義

第1回プログラム

1. Isabelle の使い方

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

2. 演習

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

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

残りの時間はチャレンジ問題と質疑応答にあてます. 問題を解きたい人は問題をやってください.質問がある人は質問してください. あとで受ける人のために答えを公表することも避けてください.これはお願いです.

講師について

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

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

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

セミナー参加の前提条件

前提知識

  • 高校の数学で習う程度の論理の知識

必要なもの

注意事項

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

連絡先

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