符号逻辑与定理机器证明PDF电子书下载

第一章　引论 1

1.1节 人工智能，符号逻辑和定理证明 1

1.2节 数学背景知识 3

参考文献 3

第二章　命题逻辑 5

2.1节　导言 5

2.2节　命题公式的解释 6

2.3节 命题逻辑的永真性和永假性 8

2.4节　命题逻辑的范式 9

2.5节　逻辑推论 12

2.6节 命题逻辑的应用 15

参考文献 18

习题 18

第三章　一阶谓词逻辑 21

3.1节 导言 21

3.2节 一阶谓词逻辑中公式的解释 24

3.3节 一阶谓词逻辑中的前束范式 27

3.4节 一阶谓词逻辑的应用 30

参考文献 32

习题 32

第四章　Herbrand定理 35

4.1节 导言 35

4.2节　Skolem标准型 36

4.3节 子句集的Herbrand全域 40

4.4节 语义树 43

4.5节　Herbrand定理 47

4.6节　Herbrand定理的实现 49

参考文献 52

习题 53

第五章　归结原理 56

5.1节 导言 56

5.2节　命题逻辑的归结原理 57

5.3节 置换与合一 59

5.4节　一致化算法 61

5.5节　一阶逻辑的归结原理 63

5.6节 归结原理的完备性 66

5.7节 应用归结原理的例子 69

5.8节 删除策略 72

参考文献 76

习题 76

第六章　语义归结与锁归结 79

6.1节 导言 79

6.2节 语义归结的非形式化讨论 79

6.3节 语义归结的形式定义及例子 81

6.4节 语义归结的完备性 82

6.5节 语义归结的特殊情况——超归结与支持集策略 84

6.6节 使用有序子句的语义归结 86

6.7节　语义归结的执行 91

6.8节 锁归结 93

6.9节 锁归结的完备性 96

参考文献 97

习题 98

第七章　线性归结 102

7.1节 导言 102

7.2节 线性归结 102

7.3节 输入归结与单元归结 103

7.4节 使用有序子句与归结基本式信息的线性归结 106

7.5节 线性归结的完备性 111

7.6节 线性演绎与树搜索 113

7.7节 树搜索中的启发式算法 118

7.8节 估价函数的估计 120

7.9节 不完备归结策略推理能力的比较 124

参考文献 129

习题 130

第八章　相等关系 133

8.1节 导言 133

8.2节 在特殊模类下的不可满足性 134

8.3节 等同归结——一个关于等词的推理规则 136

8.4节 超等同归结 138

8.5节 输入与单元等同归结 140

8.6节 线性等同归结 144

参考文献 145

习题 146

第九章　基于Herbrand定理的一些定理证明程序 149

9.1节 导言 149

9.2节 Prawitz程序 149

9.3节 V－归结程序 152

9.4节　伪语义树 158

9.5节 一个生成封闭伪语义树的算法 160

9.6节 广义Davis和Putnam分裂规则 164

参考文献 166

习题 167

第十章　程序分析 169

10.1节 导言 169

10.2节 非形式的讨论 170

10.3节 程序的形式定义 171

10.4节 描述程序执行的逻辑公式 173

10.5节 基于归结的程序分析 174

10.6节 程序的停机和响应 178

10.7节 支持集策略与停机子句的推导 180

10.8节 程序的正确性和等价性 181

10.9节 程序的特定化 182

10.10节 一个基于知识的实时程序验证策略 185

参考文献 194

习题 194

第十一章　通过演绎回答问题、问题求解和程序综合 197

11.1节 导言 197

11.2节 A类问题 198

11.3节 B类问题 199

11.4节 C类问题 201

11.5节　D类问题 203

11.6节 归结式回答问题方法的完备性 208

11.7节 程序综合原理 209

11.8节 原始归结及算法A（一个程序综合算法） 214

11.9节 算法A的正确性 222

11.10节 归纳公理在程序综合中的应用 225

11.11节 算法A（一个改进的程序综合算法） 229

参考文献 231

习题 233

第十二章　结束语 235

参考文献 236

附录A 238

A.1 一个基于单元二元归结的计算机程序 238

A.2　对该程序的简要说明 240

A.3　该计算机程序的源程序 241

A.4　程序执行示例 250

参考文献 256

附录B 257

附录C 258

文献目录 262

汉英名词对照索引 281

英汉名词对照索引 296