第1章 绪论 1
1.1 逻辑推理的发展历史 1
1.1.1 逻辑演算 3
1.1.2 证明论 5
1.1.3 模型论 8
1.1.4 递归论 9
1.1.5 公理化集合论 12
1.1.6 非单调推理理论 14
1.1.7 自动推理技术 15
1.1.8 不确定性推理 16
1.2 信念修正简介 25
1.2.1 信念状态的模型 25
1.2.2 信念变化的基本形式 28
1.2.3 信念修正理论的应用 29
1.3 自动推理理论和信念修正之间的关系 30
1.3.1 自动推理理论是实现信念修正的一种途径 31
1.3.2 信念修正可以实现非单调推理 32
参考文献 32
第2章 单调逻辑 34
2.1 命题演算逻辑系统 34
2.1.1 命题演算的基本概念 34
2.1.2 命题逻辑的合式公式及范式 37
2.2 谓词逻辑 43
2.2.1 谓词演算中的基本概念 43
2.2.2 谓词逻辑的合式公式 44
2.2.3 谓词形式系统的语义 45
2.3 逻辑演算的形式系统 47
2.3.1 公理系统 48
2.3.2 自然推理系统 54
参考文献 59
第3章 自动推理与可满足性验证 60
3.1 斯科伦标准形 61
3.2 埃尔布朗域和埃尔布朗定理 64
3.2.1 埃尔布朗域 64
3.2.2 语义树 66
3.3 DP算法 69
3.4 置换与合一 71
3.5 归结原理 74
3.5.1 命题逻辑的归结 75
3.5.2 谓词逻辑的归结 76
3.5.3 归结原理的完备性及过程控制策略 78
3.6 可满足性问题的非完全算法 82
3.7 二元可满足性问题和霍恩可满足性问题的快速算法 84
3.7.1 二元可满足性问题的快速算法 84
3.7.2 霍恩可满足性问题的快速算法 86
3.8 极大可满足问题的算法 87
3.8.1 贪心算法 87
3.8.2 局部搜索算法 87
3.8.3 模拟退火算法 88
参考文献 89
第4章 非单调推理 91
4.1 非单调逻辑产生的背景 91
4.1.1 非单调推理产生的基础 91
4.1.2 常识推理促使了非单调推理的产生 93
4.2 非单调逻辑 94
4.3 缺省逻辑 98
4.3.1 基本定义 98
4.3.2 封闭缺省理论的性质 99
4.3.3 封闭正规缺省理论 102
4.3.4 封闭正规缺省理论的证明论 104
4.4 限定逻辑 108
4.4.1 限定的定义 108
4.4.2 优先序限定 110
4.5 自认知逻辑 111
4.5.1 自知逻辑的语法 112
4.5.2 自知逻辑的语义 112
参考文献 115
第5章 信念修正理论 116
5.1 信念修正的定义 116
5.2 信念修正的AGM理论 118
5.2.1 约减和修正的合理公设 119
5.2.2 选择约减 121
5.2.3 安全约减 123
5.3 认知牢固度的方法 128
5.4 信念基的方法 130
5.5 迭代信念修正理论 133
5.5.1 基于条件函数的迭代修正 133
5.5.2 具有记忆的迭代修正 134
5.5.3 基于有限偏序牢固度秩的迭代修正 135
5.6 信念修正的应用 136
参考文献 139
第6章 单调推理技术在信念修正中的应用 141
6.1 基于核的信念基修正 141
6.1.1 核约减和修正 141
6.1.2 极小割集 143
6.1.3 计算核的算法 143
6.1.4 计算极大协调子集的算法 144
6.1.5 核和极大协调子集之间的关系 145
6.2 基于模型的修正和基于语法的修正 146
6.2.1 基于模型的方法 146
6.2.2 基于语法的方法 148
6.3 信念修正的转换系统 148
6.3.1 求极大协调子集的转换系统 148
6.3.2 求极小不协调子集的转换系统 153
6.4 基于归结的有限子句集上的信念修正实现算法 156
6.4.1 极大协调子集的方法 156
6.4.2 子句集上求所有极小不协调子集的方法 163
6.4.3 典型的信念修正方法的实现 168
6.5 信念修正的近似算法 169
6.5.1 修正的近似算法 169
6.5.2 具有完整性约束的信念修正方法 173
6.5.3 有限信念基上的修正和约减过程 175
参考文献 176
第7章 非单调推理技术在信念修正中的应用 178
7.1 信念修正和缺省推理 178
7.2 限定推理与信念修正 180
参考文献 192
第8章 信念修正的Petri网方法 193
8.1 Petri与逻辑推理 193
8.1.1 Petri网的基本概念 193
8.1.2 霍恩子句的Petri网描述 195
8.1.3 一般子句化为Petri网 198
8.2 Petri网与归结原理 200
8.2.1 霍恩基子句集的网删除归结原理 201
8.2.2 一般基子句集的网删除归结原理 207
8.3 基于Petri网的修正方法 210
8.3.1 命题规则知识库的Petri网描述 210
8.3.2 知识库更新的代数方法 213
8.3.3 扩充逻辑程序的知识库更新 228
参考文献 229