総合カリキュラムマップ
| 段階 | 領域 | 学ぶ内容 | 到達目標（コンピテンシー） |
|---|---|---|---|
| 高校〜入門 | 命題論理・集合 | 真理値、論理演算、集合の和・積・補集合 | 形式的な推論の基本・論理演算と集合の対応理解 |
| 学部前期 | 述語論理・関数・関係 | 量化子、命題と述語の区別、関数と順序 | 形式仕様を論理式で表現・集合ベースの構造理解 |
| 学部後期 | 証明系・ZFC集合論・計算理論 | 自然演繹、Hilbert系、チューリング機械 | 自動証明の原理・形式的体系の健全性の把握 |
| 学部〜大学院 | 不完全性・複雑性・形式検証 | ゲーデルの定理、P/NP、モデル検査、仕様記述 | 計算可能性・形式検証の応用設計と実装能力 |
🔹 数理論理学 Curriculum Breakdown
基礎：
- 命題論理（真理値表、論理式の同値性）
- 述語論理（量化、スコープ、項と代入）
中級：
- 証明論（Hilbert 系, 自然演繹）
- 完全性定理・健全性定理
上級：
- モデル理論（構文と意味論の一致）
- ゲーデルの不完全性定理（証明可能性 vs 真理）
🔸 集合論 Curriculum Breakdown
基礎：
- 基本演算：∪, ∩, −, ⊆
- 直積、冪集合、写像、関係の集合的定義
中級：
- 順序集合と整列集合、帰納法
- 同値関係・写像・順序の抽象的扱い
上級：
- 公理的集合論（ZFC）
- 濃度（可算無限 vs 非可算、連続体仮説）
🔹 情報学 Curriculum Breakdown
計算理論：
- 決定性有限オートマトン（DFA/NFA）
- Turing Machine, 停止問題, 計算可能関数
- 計算量クラス（P, NP, NP完全）
形式仕様と検証：
- Hoare 論理
{P} C {Q} - WP（最弱事前条件）計算、assertion
- モデル検査（CTL, LTL, NuSMV, Spin）
知識表現：
- 一階述語論理による記述
- 論理プログラミング（例：Prolog）
📘 推奨教材（段階別）
| レベル | 推奨教材（和書/洋書） |
|---|---|
| 入門 | 『論理学入門』（野矢茂樹）／ How to Prove It (Velleman) |
| 中級 | 『計算論』（渡部）／ Introduction to the Theory of Computation (Sipser) |
| 上級 | 『現代集合論入門』（坂本）／ Mathematical Logic (Enderton), Sets for Mathematicians (Pinter) |
💡 Python/ツール活用（演習・実装）
| 分野 | 活用例 | 使用ツール |
|---|---|---|
| 命題論理 | 真理値表生成、論理簡約 |
sympy.logic, z3
|
| 集合論 | Venn図、写像の可視化 |
matplotlib_venn, graphviz
|
| 計算理論 | チューリング機械エミュレータ |
turingarena, automata-lib
|
| モデル検査 | 状態遷移モデル → CTL検証 |
NuSMV, UPPAAL, TLA+
|
| 形式仕様記述 |
Z, VDM, Coq などの DSL |
🧩 相互関係まとめ図
数理論理学 ─────→ プログラム検証・AI推論
│ ↑
↓ │
集合論 ─────→ データ構造・型理論・構文意味論
│ ↑
↓ │
情報学 ─────→ 自動化・計算モデル・セキュリティ理論