論理と計算のしくみ 新装版

目次

1. はしがき 学習の手引 １ 集合と関係 1.1 集 合 (a)集 合 (b)空集合 (c)部分集合 (d)結びと交わり (e)直積と直和 (f)関数空間とベキ集合 (g)集合族 (h)∏ と ∑ 1.2 関 係 (a)二項関係 (b)合成と閉包 (c)順 序 (d)束 (e)同値関係 ２ 命題論理と述語論理 2.1 命題論理 (a)命 題 (b)論理記号 (c)構文論 (d)意味論 (e)コンパクト性 (f)ヒルベルト流 (g)シーケント計算 (h)導出原理 2.2 一階述語論理 (a)構文論 (b)意味論 (c)エルブランの定理 (d)ヒルベルト流 (e)シーケント計算 (f)導出原理 (g)等号付き一階述語論理 2.3 高階述語論理とその部分体系 (a)二階述語論理 (b)後継者のみの単項二階論理 (c)高階述語論理 ３ 様相論理と直観主義論理 3.1 命題様相論理 (a)構文論 (b)意味論 (c)シーケント計算 (d)有限モデル性 (e)さまざまな様相論理 3.2 多重様相論理 (a)構文論 (b)意味論 (c)多重様相論理の例 (d)反射推移閉包 3.3 時相論理 (a)分岐時間時相論理 (b)線形時間時相論理 (c)線形時間vs.分岐時間 (d)様相μ計算 (e)モデル検査 3.4 命題直観主義論理 (a)構文論 (b)意味論 (c)直観主義論理の真偽値 (d)シーケント計算 ４ 計算可能性 4.1 チューリング機械 (a)チューリング機械 (b)計算可能関数 4.2 帰納的関数 (a)原始帰納的関数 (b)部分帰納的関数 (c)停止問題 (d)帰納的集合 (e)算術的階層 4.3 不完全性定理 (a)算 術 (b)表現可能性 (c)符号化 (d)ゲーデルの不完全性定理 (e)第二不完全性定理 4.4 プレスバーガ算術 (a)構文論と意味論 (b)限定子除去 4.5 述語論理の決定不能性と決定可能な部分体系 (a)一階述語論理の決定不能性 (b)単項一階述語論理 (c)等号付き単項一階述語論理 (d)一階述語論理のガード付きフラグメント (e)後継者のみの単項二階論理 ５ λ計算 5.1 λ 項 (a)再帰的関数 (b)λ式 (c)λ項 5.2 簡 約 (a)β簡約 (b)β簡約の例 (c)チャーチ ロッサーの定理 (d)チャーチ ロッサーの定理の証明 (e)標準化 (f)評価戦略 (g)η簡約 5.3 型付きλ計算 (a)型 (b)型付け (c)β簡約と型付け (d)正規化可能性 (e)明示的型付けと暗黙的型付け (f)型推論 (g)自然演繹 (h)カリー ハワードの対応 (i)多相型 章末問題解答 索 引