第一章 引论 1
1.1节 人工智能，符号逻辑和定理证明 1
1.2节 数学背景知识 3
参考文献 3
第二章 命题逻辑 5
2.1节 导言 5
2.2节 命题公式的解释 6
2.3节 命题逻辑的永真性和永假性 8
2.4节 命题逻辑的范式 9
2.5节 逻辑推论 12
2.6节 命题逻辑的应用 15
参考文献 18
习题 18
第三章 一阶谓词逻辑 21
3.1节 导言 21
3.2节 一阶谓词逻辑中公式的解释 24
3.3节 一阶谓词逻辑中的前束范式 27
3.4节 一阶谓词逻辑的应用 30
参考文献 32
习题 32
第四章 Herbrand定理 35
4.1节 导言 35
4.2节 Skolem标准型 36
4.3节 子句集的Herbrand全域 40
4.4节 语义树 43
4.5节 Herbrand定理 47
4.6节 Herbrand定理的实现 49
参考文献 52
习题 53
第五章 归结原理 56
5.1节 导言 56
5.2节 命题逻辑的归结原理 57
5.3节 置换与合一 59
5.4节 一致化算法 61
5.5节 一阶逻辑的归结原理 63
5.6节 归结原理的完备性 66
5.7节 应用归结原理的例子 69
5.8节 删除策略 72
参考文献 76
习题 76
第六章 语义归结与锁归结 79
6.1节 导言 79
6.2节 语义归结的非形式化讨论 79
6.3节 语义归结的形式定义及例子 81
6.4节 语义归结的完备性 82
6.5节 语义归结的特殊情况——超归结与支持集策略 84
6.6节 使用有序子句的语义归结 86
6.7节 语义归结的执行 91
6.8节 锁归结 93
6.9节 锁归结的完备性 96
参考文献 97
习题 98
第七章 线性归结 102
7.1节 导言 102
7.2节 线性归结 102
7.3节 输入归结与单元归结 103
7.4节 使用有序子句与归结基本式信息的线性归结 106
7.5节 线性归结的完备性 111
7.6节 线性演绎与树搜索 113
7.7节 树搜索中的启发式算法 118
7.8节 估价函数的估计 120
7.9节 不完备归结策略推理能力的比较 124
参考文献 129
习题 130
第八章 相等关系 133
8.1节 导言 133
8.2节 在特殊模类下的不可满足性 134
8.3节 等同归结——一个关于等词的推理规则 136
8.4节 超等同归结 138
8.5节 输入与单元等同归结 140
8.6节 线性等同归结 144
参考文献 145
习题 146
第九章 基于Herbrand定理的一些定理证明程序 149
9.1节 导言 149
9.2节 Prawitz程序 149
9.3节 V－归结程序 152
9.4节 伪语义树 158
9.5节 一个生成封闭伪语义树的算法 160
9.6节 广义Davis和Putnam分裂规则 164
参考文献 166
习题 167
第十章 程序分析 169
10.1节 导言 169
10.2节 非形式的讨论 170
10.3节 程序的形式定义 171
10.4节 描述程序执行的逻辑公式 173
10.5节 基于归结的程序分析 174
10.6节 程序的停机和响应 178
10.7节 支持集策略与停机子句的推导 180
10.8节 程序的正确性和等价性 181
10.9节 程序的特定化 182
10.10节 一个基于知识的实时程序验证策略 185
参考文献 194
习题 194
第十一章 通过演绎回答问题、问题求解和程序综合 197
11.1节 导言 197
11.2节 A类问题 198
11.3节 B类问题 199
11.4节 C类问题 201
11.5节 D类问题 203
11.6节 归结式回答问题方法的完备性 208
11.7节 程序综合原理 209
11.8节 原始归结及算法A（一个程序综合算法） 214
11.9节 算法A的正确性 222
11.10节 归纳公理在程序综合中的应用 225
11.11节 算法A（一个改进的程序综合算法） 229
参考文献 231
习题 233
第十二章 结束语 235
参考文献 236
附录A 238
A.1 一个基于单元二元归结的计算机程序 238
A.2 对该程序的简要说明 240
A.3 该计算机程序的源程序 241
A.4 程序执行示例 250
参考文献 256
附录B 257
附录C 258
文献目录 262
汉英名词对照索引 281
英汉名词对照索引 296