目次

まえがき

構造と方法
原書第三版での変更点
読者へ
補助教材
本書の利用法
謝辞
訳者まえがき

第6 章初等論理

6.1 どのように推論するか
6.2 命題計算
　　　6.2.1 整論理式と意味
　　　6.2.2 論理的同値
　　　6.2.3 真理値関数と標準形
　　　6.2.4 論理結合子の十分な集合
6.3 形式的推論
　　　6.3.1 証明規則
　　　6.3.2 証明
　　　6.3.3 導出される規則
　　　6.3.4 定理そして健全性と完全性
　　　6.3.5 実践により完璧となる
6.4 形式的公理システム
　　　6.4.1 公理システムの例
　　　6.4.2 他の公理システム
6.5 章のまとめ
　　　注釈

第7 章述語論理

7.1 一階述語計算
　　　7.1.1 述語と限量子
　　　7.1.2 整論理式
　　　7.1.3 解釈と意味
　　　7.1.4 妥当性
　　　7.1.5 妥当性問題
7.2 同値式
　　　7.2.1 論理同値性
　　　7.2.2 標準形
　　　7.2.3 英語の文を形式化する
　　　7.2.4 まとめ
7.3 述語計算における形式的証明
　　　7.3.1 全称実体化（Universal Instantiation：UI）
　　　7.3.2 存在汎化（Existential Generalization：EG）
　　　7.3.3 存在実体化（Existential Instantiation, EI）
　　　7.3.4 全称汎化（Universal Generalization, UG）
　　　7.3.5 形式的証明の例
7.4 章のまとめ
　　　註釈

第8 章応用論理

8.1 等価性
　　　8.1.1 等価性を記述する
　　　8.1.2 等しいものによる置換を拡張する
8.2 プログラムの正当性
　　　8.2.1 命令型プログラムの正当性
　　　8.2.2 配列代入
　　　8.2.3 停止性
　　　注釈
8.3 高階論理
　　　8.3.1 高階論理を分類する
　　　8.3.2 意味論
　　　8.3.3 高階推論
8.4 章のまとめ

第9 章計算論理

9.1 自動推論
　　　9.1.1 節と節形式
　　　9.1.2 命題の導出
　　　9.1.3 代入と単一化
　　　9.1.4 導出：一般的な場合
　　　9.1.5 導出による定理証明
　　　9.1.6 注意
9.2 論理プログラミング
　　　9.2.1 家系図
　　　9.2.2 論理プログラムの定義
　　　9.2.3 導出と論理プログラミング
　　　9.2.4 計算の木
　　　9.2.5 論理プログラミングの技法
　　　9.2.6 証明できないことについての注意
9.3 章のまとめ

第10 章代数構造と技法

10.1 代数とはなにか
　　　10.1.1 代数の定義
　　　10.1.2 具象と抽象
　　　10.1.3 代数に慣れる
10.2 ブール代数
　　　10.2.1 ブール式を簡約する
　　　10.2.2 ディジタル回路
10.3 代数としての抽象データ型
　　　10.3.1 自然数
　　　10.3.2 リストと文字列
　　　10.3.3 スタックとキュー
　　　10.3.4 二分木と優先度付きキュー
10.4 計算代数
　　　10.4.1 関係代数
　　　10.4.2 関数代数
10.5 様々な代数的アイデア
　　　10.5.1 合同
　　　10.5.2 暗号：RSA アルゴリズム
　　　10.5.3 部分代数
　　　10.5.4 準同型写像
10.6 章のまとめ

付録

ギリシャ文字
記号
参考文献