第一章 表列方法及其发展 1
第一节 逻辑证明系统与逻辑语义 1
一、“正确推理”的两种定义 1
二、语言层面的语形和语义 3
三、逻辑层面的语形和语义 5
四、逻辑证明系统 8
五、逻辑证明系统的基本性质 11
第二节 表列系统 13
一、逻辑表列的基本思想 13
二、表列的实施——树 16
三、表列方法的优点 19
第三节 表列方法的发展 21
第二章 命题逻辑的表列方法 28
第一节 命题逻辑的形式语言：句法 28
一、形式语言？p 28
二、公式的构造树 30
三、？p-公式的归纳原理和递归原理 33
第二节 语义：真值指派与赋值 35
一、真值函数 35
二、真值指派与布尔赋值 36
三、饱和集 39
第三节 命题逻辑的Smullyan表列 40
一、加标公式表列 40
二、不加标公式表列 43
三、统一记法 44
四、扩充系统 45
第四节 Smullyan命题逻辑表列的可靠性与完全性 47
一、可靠性 47
二、完全性 48
三、流畅性与紧致性 51
第五节 Smullyan命题逻辑表列的优化 52
一、简化Smullyan表列的若干技巧 52
二、Smullyan表列的冗余问题 55
三、Smullyan表列的优化 57
第六节 表列系统KE 60
第三章 一阶逻辑的表列方法 63
第一节 一阶逻辑的句法 63
一、？的初始符号 64
二、？-表达式 64
三、？-表达式的唯一可读性 67
第二节 一阶逻辑的语义：模型和赋值 70
一、一阶模型和变元指派 70
二、Herbrand-模型 73
第三节 一阶公式的变形及其语义性质 74
一、变元的代入 75
二、Skolem-公式 77
三、子句公式 78
第四节 一阶句子表列 79
一、一阶句子表列 79
二、一阶句子表列的可靠性和完全性 84
三、一阶句子表列的Herbrand优化 88
第五节 自由变元表列 89
一、合一 91
二、自由变元表列 93
第六节 子句表列 101
一、析取子句表列 101
二、蕴涵子句表列 103
第四章 一阶等词理论推理的表列 107
第一节 理论和理论推理 108
一、理论 108
二、理论推理的基本概念 109
第二节 等词理论推理的表列 111
一、句子型等词理论推理表列 111
二、理论推理的自由变元表列 114
三、带全称变元的理论推理表列 116
第三节 理论推理表列的可靠性和完全性 119
一、可靠性 119
二、完全性 121
第四节 基于Reeves方法的ε-表列的改进 128
第五章 模态逻辑的表列方法 132
第一节 模态逻辑的形式语言和公理系统 133
一、模态逻辑的形式语言 133
二、正规模态逻辑的公理系统 134
第二节 Kripke语义：模型和框架 136
一、模型和框架 136
二、模态公式与和框架性质（一阶公式）的对应 138
第三节 模态语义图 139
一、Kripke语义图 139
二、加标语义图 142
三、D、T、S4、B和S5的语义图 144
四、模态语义图的可靠性和完全性 147
第四节 隐性模态表列 149
一、K、D、T、S4的分析性表列 150
二、B和S5的准分析性表列 153
三、Fitting模态表列系统的可靠性和完全性 158
四、似矢列演算的模态表列系统CK、CD、CT、CS4、CB和CS5 161
第五节 前缀模态表列 169
第六节 Massacci的一步模态表列SST 175
第七节 前缀模态表列系统KEM 178
一、前缀 178
二、前缀的合一 179
三、KEM表列规则 182
第六章 非单调逻辑的表列方法 185
第一节 缺省逻辑及其表列方法 186
一、Reiter的缺省逻辑 187
二、其他缺省逻辑 190
三、缺省逻辑的表列方法 193
第二节 非单调模态逻辑及其表列方法 199
一、Moore的自认知逻辑 199
二、自认知逻辑的表列证明 202
三、多模态非单调逻辑H的表列 205
第三节 正常条件句逻辑KLM的表列演算 209
一、正常条件句逻辑KLM 209
二、优先逻辑P 211
三、P的扩充及其表列演算 213
第四节 限定逻辑的表列方法 216
一、从谓词限定到公式限定 217
二、命题限定逻辑表列 221
三、公式限定逻辑的子句表列 225
参考文献 229
符号索引 233