科学技術と共に歩む

1.　推論の形式化：自然演繹
1.1　推論の形式化とは
1.2　述語計算
　　1.2.1　項
　　1.2.2　式
　　1.2.3　メタ変数
　　1.2.4　部分式，出現，自由変数，束縛変数
　　1.2.5　アルファ同値性，代入
　　1.2.6　証明
　　1.2.7　sequent，証明可能性，定理
　　1.2.8　sequentの証明可能性
　　1.2.9　代入法則
　　1.2.10　式の等号法則
　　1.2.11　論理記号の定義
　　1.2.12　等号付き述語計算
1.3　応用述語計算
1.4　理論
演習問題
2.　形式的言語の意味論と推論法則の妥当性
2.1　意味論とは
2.2　古典論理の意味論
　　2.2.1　NKの意味論の形式的定義
　　2.2.2　アルファ同値性の妥当性
　　2.2.3　NKの健全性
2.3　構成的論理の意味論
2.4　応用述語計算の意味論
演習問題
3.　証明の標準化
3.1　証明の標準化とは
　　3.1.1　証明の回り道の除去
　　3.1.2　帰約可能点，標準形
　　3.1.3　証明の変数，ラベルの自由出現，束縛出現
　　3.1.4　証明のアルファ同値性，証明への代入
3.2　標準化定理の証明
　　3.2.1　標準化木
　　3.2.2　計算可能性集合
　　3.2.3　標準化定理
3.3　NJの標準化定理の応用
演習問題
4.　sequent calculus
4.1　sequent calculusとは
4.2　sequent calculus
　　4.2.1　LJ，LK
4.3　基本定理
4.4　LJの基本定理の証明と標準形定理
　　4.4.1　標準化定理から基本定理へ
　　4.4.2　基本定理から標準化定理へ
4.5　LKの完全性定理と基本定理の証明
　　4.5.1　探索列
　　4.5.2　探索木
　　4.5.3　完全性定理と基本定理
演習問題
5.　分解原理
5.1　分解原理とは
5.2　Skolem標準形
5.3　Herbrandの定理
5.4　基本分解原理
　　5.4.1　節，節集合
　　5.4.2　基本分解原理
　　5.4.3　基本分解原理の健全性と完全性
　　5.4.4　基本分解原理による定理自動証明
5.5　一般分解原理
　　5.5.1　分解による項の選択
　　5.5.2　統一化
　　5.5.3　一般分解原理による証明
　　5.5.4　一般解の存在証明，統一化アルゴリズム
演習問題
6.　Curry-Howardの対応
6.1　Curry-Howardの対応とは
6.2　型付き言語F0
　　6.2.1　F0のプログラムと型
　　6.2.2　プログラムの実行
6.3　NJのサブセットL0とF0の対応
　　6.3.1　式と型の対応
　　6.3.2　証明とプログラムの対応
　　6.3.3　プログラムの実行と証明の帰約の対応
　　6.3.4　Curry-Howardの対応のまとめ
演習問題
付録
参考文献
索引