《基于归结方法的自动推理》求取 ⇩

前言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 一阶模态归结系统FMRD480

14．5 命题模态归结弱包含删除策略486

参考文献495