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

構成数 : 1

はしがき
学習の手引

1 集合と関係
1.1 集 合
(a)集 合
(b)空集合
(c)部分集合
(d)結びと交わり
(e)直積と直和
(f)関数空間とベキ集合
(g)集合族
(h)∏ と ∑
1.2 関 係
(a)二項関係
(b)合成と閉包
(c)順 序
(d)束
(e)同値関係

2 命題論理と述語論理
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 様相論理と直観主義論理
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 計算可能性
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 λ計算
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)多相型

章末問題解答
索 引