符号逻辑与定理机器证明2025|PDF|Epub|mobi|kindle电子书版本百度云盘下载

符号逻辑与定理机器证明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

附录A238

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

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

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

A.4　程序执行示例250

参考文献256

附录B257

附录C258

文献目录262

汉英名词对照索引281

英汉名词对照索引296