前言 1
绪论 1
前言页 1
第一部分 古典逻辑中的归结推理 9
第一章 一阶（谓词）逻辑 9
1．1 引言 9
1．2 谓词与量词 11
1．3 公式及解释 15
1．4 等价和蕴涵 17
1．5 范式 18
1．6 形式推理 27
2．1 子句集的Herbrand域 31
第二章 归结同理 31
2．2 Herbrand定理 36
2．3 合一算法 43
2．4 归结原理及其完备性定理 55
2．5 将Resolution Principle翻译成归结原理的原因 64
2．6 删除策略 66
第三章 语义归结、线性归结、锁归结 75
3．1 语义归结 75
3．2 线性归结 85
3．3 锁归结 102
3．4 输入归结与单元归结 107
4．1 引言 113
第四章 处理等词的调解法 113
4．2 相等公理与E—恒假 116
4．3 调解与E蕴涵 119
4．4 P超调解 121
4．5 RUE－NRF归结及其strong形的反例 124
4．6 对称调解 138
4．7 线性对称调解的完备性 143
4．8 RUE－NRF归结与调解的关系 150
第五章 归结方法间的相容性问题 159
5．1 线性归结和语义归结不相容 160
5．2 锁归结和语义归结的相容性 161
5．3 锁归结与线性归结的相容性 170
5．4 用约化代替取因子 174
5．5 着色归结 179
第六章 广义归结 191
6．1 广义归结 192
6．2 广义锁归结 196
6．3 广义线性归结 199
6．4 广义语义归结 205
6．5 广义线性半锁归结 207
6．6 广义删除策略 211
6．7 NC归结 222
6．8 广义归结与NC归结 228
6．9 广义归结施行删除策略的结果——NC归结 236
6．10 排除自归结的归结原理 245
7．1 1型广义调解 247
第七章 广义调解 247
7．2 2型广义调解和广义线性对称调解 252
7．3 NC调解与NC线性对称调解 256
7．4 广义RUE－NRF归结 263
7．5 NC－RUE－NRF归结 268
第八章 Horn集上的归结方法 274
8．1 正单元有序归结 275
8．2 强有序输入归结 283
8．3 输入半锁归结和单元锁归结 293
8．4 输入对称调解和单元对称调解 297
8．5 输入有向调解和单元有向调解 308
8．6 广义Horn集 313
9．1 引言 325
第二部分 非标准逻辑中的归结推理 325
第九章 模糊逻辑 325
9．2 真值取在格上的模糊逻辑 329
9．3 模糊归结 340
第十章 算子模糊逻辑（算子格上） 347
10．1 引言 347
10．2 算子格 348
10．3 算子格上的逻辑系统 349
10．4 λ－归结方法 356
10．5 λ－弱蕴涵和λ－强蕴涵 361
10．6 对算子模糊逻辑的解释 368
10．7 结合算子格及λ■－归结 374
10．8 广义λ－归结及其删除策略 386
11．1 引言 399
第十一章 算子模糊逻辑（布尔代数上） 399
11．2 布尔代数上的Fuzzy算子运算 400
11．3 布尔算子模糊逻辑 403
11．4 λ－归结方法 408
11．5 BOFL系统的一个简单解释 412
13．1 引言 413
第十二章 处理模糊相等的λ－调解法 417
12．1 引言 417
12．2 模糊相等公理集 418
12．3 锁λ－调解法和线性λ－调解法 420
12．4 广义λ－调解 427
第十三章 非单调逻辑 433
13．2 缺省理论及其扩充 434
13．3 正规缺省理论 439
13．4 证明理论 443
13．5 非单调逻辑中的归结方法 448
第十四章 模态逻辑中的归结推理 452
14．1 模态逻辑 453
14．2 命题模态归结推理 455
14．3 一阶模态归结推理 468
14．4 一阶模态归结系统FMRD 480
14．5 命题模态归结弱包含删除策略 486
参考文献 495