セミナーの内容

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

第2回では、1階述語論理を扱えるように定理証明器を拡張します。以下のような証明ができるようになります：

# 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(x2)
# apply (allL "x2");;
0. P --> Q(x2), ALL x. P --> Q(x), P |- Q(x2)
# apply impL;;
0. ALL x. P --> Q(x), P |- P, Q(x2)
1. Q(x2), ALL x. P --> Q(x), P |- Q(x2)
# apply assumption;;
0. Q(x2), ALL x. P --> Q(x), P |- Q(x2)
# apply assumption;;
No subgoals!

1階述語論理の難所は、量化子の推論規則についている付帯条件です。この部分をプログラムすることで理解を深めることができると思います。

シリーズ全3回の予定

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

プログラム

1. シーケント計算による1階述語論理：構文と推論規則
2. 定理証明器の設計
3. リファレンス実装の解説
4. 実装の相談

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

必要なもの

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

Zoom URL

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

配布物

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

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

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

注意事項

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

連絡先

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