第一章引论 1
目 录 1
§1.1什么是自动推理 2
§1.2 各章简介 4
第二章从例子学逻辑 7
§2.1逻辑运算 7
§2.2 自动推理程序使用的语言 12
2.2.1谓词和常量 14
2.2.2变量 15
2.2.3 函数 17
§2.3转换规则 21
2.4.1假设和公理 23
§2.4假设和公理、推理类型以及证明 23
2.4.2推理的的类型——推理规则 25
2.4.3证明 28
§2.5小结 35
第三章智力问题 37
§3.1小型的工作智力问题 38
3.1.1小型工作智力问题的表示方法 39
3.1.2选择推理的类型 41
3.1.3小型工作智力问题的解 41
3.1.4关于子句描述和证明的讨论 45
§3.2完整的工作智力问题 46
3.2.1人的求解过程 47
3.2.2用自动推理程序的求解过程 50
3.2.3小结 75
第四章 灵活的表示方法和等式的应用 77
§4.1信息表示的一般化 78
§4.2技巧与直接方法 86
§4.3相等 93
4.3.1小型方块排列问题 97
4.3.2完整的方块排列问题 100
§4.4推理程序中的操作顺序 104
§4.5格外小心 111
第五章疑难智力问题 113
§5.1棋盘和骨牌智力问题 113
5.1.1人的推理 114
5.1.2问题的表示 115
5.1.3推理规则的选择 123
5.1.4求解策略 123
5.1.5求解方法的性质和结果 124
§5.2传教士与野人智力问题 126
5.2.1问题的简单表示 127
5.2.2问题的复杂表示 129
§5.3弹子和天平智力问题 137
5.3.1问题的表示 138
第六章小结 149
§6.1逻辑 149
6.1.1and（与） 149
6.1.3 not（非） 150
6.1.2 or（或） 150
6.1.4if-then（如果—则） 151
6.1.5 is-equiualent-to（等价） 151
6.1.6关系与法则 151
§6.2描述语言 153
6.2.1变量 154
§6.3问题描述 155
6.3.1假设和公理 156
6.3.2特殊事实和特殊假设 156
6.3.3 目标或定理的否定 156
§6.4推理规则 158
6.4.1合 158
6.4.2二元归结 159
6.4.3 UR-归结 160
6.4.4超归结 160
6.4.5等式归结 161
6.4.6其它推理推则 163
§6.5空子句 163
§6.6 归约（Demodulation） 164
§6.7类含检查（Subsumption） 166
§6.8控制策略 167
6.8.1支撑集策略 167
6.8.2加权策略 168
6.8.3单位子句优先策略 168
§6.9推理实例 169
§6.10 AURA 172
第七章逻辑电路设计 177
§7.1逻辑电路设计基本方法 177
7.1.1基本逻辑电路 177
7.1.2设计说明 181
§7.2逻辑电路设计中的归约方法 183
7.2.1函数型设计说明 183
7.2.2描述性设计说明 187
7.2.3表格型设计说明 189
7.2.4 电路设计中归约方法的利弊 191
§7.3逻辑电路设计中的超归结方法 192
7.3.1 谓词OUTPUT 192
7.3.2构造规则 193
7.3.3例子 194
7.3.4 可达信号与谓词OUTPUT 197
§7.4迷宫电路的求解 198
7.4.1复杂性分析 198
7.4.2方法1 200
7.4.3方法2 204
7.4.4方法3 208
§7.5多值逻辑设计中的负超归结方法 214
7.5.1 T门 215
7.5.2多值函数的表示 215
7.5.3构造规则 217
7.5.4负超归结 217
§8.2一个简单的例子 221
第八章 逻辑电路的正确性证明 221
§8.1 什么是逻辑电路的正确性证明 221
§8.3例子的重要特征 224
8.3.1语言翻译 224
8.3.2规范化 225
8.3.3简化 226
8.3.4交换型归约式和字典排序 226
§8.4更复杂的例子 228
§8.5加法器电路的证明 234
8.5.1 1位全加器 234
8.5.2黑箱技术 239
第九章数学研究 242
§9.1 简例 243
9.1.1支撑集策略的应用 249
9.1.2加权策略的应用 252
9.1.3归约和规范 254
9.1.4类含和冗余 255
§9.2疑难问题的求解 261
§9.3模型和反例的生成 264
§9.4概念的可表示性：难和易 271
§9.5 小结 272
第十章形式逻辑的研究 275
§10.1等价演算 276
§10.2一个简单例子 277
§10.3给以知识和直觉 280
§10.4解答疑难问题 282
10.4.1寻找有用的记法 284
10.4.2提出猜想 285
第十一章专家系统 289
§11.1 什么是专家系统 289
§11.2博奕专家系统 290
§11.3其它类型的专家系统 292
§11.4推理元 293
§11.5简单的专家系统 297
§11.6专家系统中推理的深度 306
§11.7 小结 311
第十二章程序排错与验证 312
12.1.1程序段的推理 314
§12.1符号执行 314
12.1.2符号执行程序的表示 316
12.1.3模拟程序执行的归约式 326
12.1.4正确程序的执行 333
12.1.5错误程序段的符号执行 334
§12.2程序正确性证明 338
12.2.1一简单程序及其说明 340
12.2.2证明无循环程序的正确性 341
12.2.3条件语句的正确性证明 345
12.2.4循环程序的正确性证明 348
12.2.5证明循环出口处的正确性 352
12.2.6程序的正确性 354
12.2.7含数组的程序的正确性的证明 356
§12.3抽象程序设计和高级程序证明 360
1 2.3.1什么叫抽象程序设计 361
12.3.2一个抽象程序设计的例子 363
§12.4结论 370
第十三章Prolog：逻辑程序设计语言 372
§13.1 Prolog简介 374
§13.2核反应堆设计中的一例 386
13.2.1问题的描述 386
13.2.2用Prolog表示事实 393
13.2.3一个验证连接点属性的简单程序 398
13.2.4寻找路径 399
13.2.5检查单个部件引起的失灵 400
§13.3小结 402
第十四章 自动推理的形式处理 404
§14.1语言 404
§14.2推理规则 408
14.2.1二元归结 411
14.2.2完备性 415
§14.3策略 422
§14.4其他推理规则 429
§14.5类含检查 436
§14.6归约法 438
第十五章 自动推理艺术 440
§15.1信息的表示 442
15.1.1单位子句 443
15.1.2相等谓词 446
15.1.3短子句优于长子句 447
15.1.4相关信息 448
§15.2推理规则 449
§15.3控制策略 451
§15.4文献说明 454
第十六章默认推理 455
§16.1默认推理实例 455
16.1.1默认推理的非单调特征 459
16.1.2默认和伤残知识 460
§16.2默认理论及其延伸 462
16.2.1预备知识 462
16.2.2封闭默认理论的延伸 463
§16.3规范默认理论 470
16.3.1封闭规范默认理论 471
§16.4证明理论 477
16.4.1默认证明 478
16.4.2延伸元的判定问题 485
§16.5 目标驱动的默认证明：和归结证明器的关系 487
§16.6封闭规范默认理论和信念修正 495
16.6.1公共延伸 496
16.6.2信念的产生和新信息的同化 499
16.6.3信念的产生和新默认的同化 499
§16.7小结 500
参考文献 503