セミナーの内容

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

第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 までお気軽にご連絡ください．