基于归结方法的自动推理PDF电子书下载

前言 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