定理証明器を作って学ぶ論理学 第3回 単一化(全3回)

2024/07/18(木)19:30 〜 21:00 開催
ブックマーク

イベント内容

セミナーの内容

定理証明器を作ることで、論理学を深く理解しようというセミナーです。参加者が好きなプログラミング言語で実装できるように、しくみと作りかたを解説します。

第2回で作った定理証明器では、∀-left と ∃-right の推論規則において具体化する項をユーザが指定する必要がありました。第3回では、単一化 (unification) というしくみを使って、項が自動的に選択されるように拡張します。結果として、次のような証明が書けるようになります:

theorem "(ALL x. P --> Q(x)) --> (P --> (ALL x. Q(x)))";;
0.  |- (ALL x. P --> Q(x)) --> P --> (ALL x. Q(x))
# apply impR;;
0. ALL x. P --> Q(x) |- P --> (ALL x. Q(x))
# apply impR;;
0. P, ALL x. P --> Q(x) |- ALL x. Q(x)
# apply allR;;
0. P, ALL x. P --> Q(x) |- Q(_0)
# apply allL;;
0. P --> Q(?_1), ALL x. P --> Q(x), P |- Q(_0)
# apply impL;;
0. ALL x. P --> Q(x), P |- P, Q(_0)
1. Q(?_1), ALL x. P --> Q(x), P |- Q(_0)
# apply assumption;;
0. Q(?_1), ALL x. P --> Q(x), P |- Q(_0)
# apply assumption;;
[?_1 -> _0]
No subgoals!

シリーズ全3回の予定

  • 第1回 命題論理
  • 第2回 1階述語論理
  • 第3回 単一化(ユニフィケーション)

プログラム

  1. 項を自動的に選択するためのしくみ
  2. 定理証明器の設計
  3. リファレンス実装の解説
  4. 実装の相談

講師について

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

プロセス代数 CSP に基づいた検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「モデル検査特論」講師

セミナー参加の前提条件

前提知識

  • 1階述語論理の基本的な知識:項、変項、関数、述語、量化子(全称量化、存在量化)

必要なもの

  • 使用するプログラミング言語の開発環境(リファレンス実装を動かすためには OCaml の開発環境が必要です)

Zoom URL

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

配布物

スライド資料(PDF)とリファレンス実装のソースコード(OCaml)を CONNPASS のメッセージにて送付します.

プログラムの大きさの目安

定理証明器のコードの大きさは、OCaml のリファレンス実装で約600行程度です。前回からの増加分は約200行です。

注意事項

  • 講師が知らないプログラミング言語については対処が限られます.
  • 配布資料の公開は禁止です.

連絡先

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

注意事項

※ こちらのイベント情報は、外部サイトから取得した情報を掲載しています。
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。
情報提供元ページ(connpass)へ

新規会員登録

このイベントに申し込むには会員登録が必要です。
アカウント登録済みの方はログインしてください。



※ ソーシャルアカウントで登録するとログインが簡単に行えます。

※ 連携したソーシャルアカウントは、会員登録完了後にいつでも変更できます。

関連するイベント