目录

第一章 符号逻辑

1.1 命题逻辑

1.2 一阶逻辑

第二章 Herbrand定理

2.1 skolem标准型

2.2 子句集的Herbrand域

2.3 语义树

2.4 Herbrand定理

第三章 归结原理

3.1 命题逻辑中的归结原理

3.2 替换与合一替换

3.3 一阶逻辑中的归结原理

3.4 归结原理的完备性

3.5 删除策略

3.6 用约化代替取因子

第四章 锁归结和线性归结

4.1 锁归结原理

4.2 线性归结原理

4.3 线性归结的完备性

4.4 输入归结和单元归结

4.5 线性归结的实现

第五章 语义归结和锁语义归结

5.1 概念的引进

5.2 语义归结原理的完备性

5.3 使用有序子句的语义归结

5.4 语义归结的实现

5.5 锁语义归结原理——IDI归结

5.6　锁语义归结原理——LI归结

6.1 引言

第六章　广义归结原理

6.2　广义归结方法

6.3　广义锁归结方法

6.4　广义线性归结方法

6.5　广义语义归结方法

6.6　删除策略的变型

6.7　广义归结中的删除策略

第七章　模糊逻辑和模糊归结原理

7.1 引言

7.2　模糊逻辑

7.3　模糊逻辑中的归结原理

7.4 FLI归结原理

7.5 几点注记

第八章 自然推导

8.1 skolem化过程

8.2 自然推导规则

8.3 自然推导法的可靠性

8.4 自然推导法的推广

8.5 自然推导法的不完备性

第九章 重写规则法

9.1 重写规则与Knuth-Bendix算法

9.2 布尔代数标准重写系统

9.3 BN合一与重写证明算法

9.4 重写证明算法的完备性

第十章 机器证明的数学归纳法

10.1 基本概念

10.2 归纳法原理

10.3 定义原理

10.4 Boyer-Moore定理证明系统概述

参考文献