高阶逻辑辅助证明系统PDF|Epub|txt|kindle电子书版本网盘下载

高阶逻辑辅助证明系统PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

第一部分 基本技巧3

第一章 基础3

1.1 引言3

1.2 theory（理论）4

1.3 类型，项和公式5

1.4 变元8

1.5 交互与界面8

1.6 启动9

第二章 HOL中的函数编程10

2.1 theory简介10

2.2 求值13

2.3 证明简介13

小结18

2.4 一些有用的命令19

2.5 数据类型19

2.5.1 表（1ist）20

2.5.2 一般格式20

2.5.3 原始递归21

2.5.4 case表达式22

2.5.5 结构归纳和case分支22

2.5.6 实例学习：布尔表达式23

2.6 一些基本类型27

2.6.1 自然数27

2.6.2 有序对29

2.6.3 option类型29

2.7 定义30

2.7.1 类型同名30

2.7.2 常量定义30

2.8 定义方法31

第三章 高级函数式编程32

3.1 化简32

3.1.1 什么是化简？32

3.1.2 化简规则33

3.1.3 simp方法34

3.1.4 添加或删除化简规则34

3.1.5 假设34

3.1.6 用定义重写35

3.1.7 let－表达式化简36

3.1.8 条件化简规则37

3.1.9 自动Case分解37

3.1.1 0追踪39

3.1.1 1寻找定理41

3.2 启发式归纳42

3.3 案例学习：编译表达式45

3.4 高级数据类型48

3.4.1 互递归48

3.4.2 嵌套递归51

3.4.3 嵌套递归的限制53

3.4.4 案例学习：Tries（特里树）55

3.5 完全递归函数59

3.5.1 定义59

3.5.2 终止性60

3.5.3 化简61

3.5.4 归纳63

第四章 theory的表示65

4.1 具体语法65

4.1.1 中缀记号65

4.1.2 数学符号66

4.1.3 前缀记号68

4.1.4 简写69

4.2 文档编制70

4.2.1 Isabelle会话71

4.2.2 结构标记73

4.2.3 形式评注与反引式75

4.2.4 符号的释义78

4.2.5 抑制输出78

第二部分 逻辑与集合83

第五章 游戏规则83

5.1 自然演绎推理83

5.2 引入规则84

5.3 消去规则85

5.4 破坏性规则：一些例子88

5.5 蕴含89

5.6 否定91

5.7 中间处理：规则处理的基本方法93

5.8 合一与替换95

5.8.1 替换与subst方法96

5.8.2 合一及其陷阱98

5.9 量词100

5.9.1 全称引入规则100

5.9.2 全称消去规则101

5.9.3 存在量词103

5.9.4 绑定变元改名：rename tac103

5.9.5 重用假设：frule104

5.9.6 量词的显式实例化105

5.10 描述算子107

5.10.1 确定描述107

5.10.2 不确定描述108

5.11 一些失败的证明110

5.12 使用blast方法证明定理112

5.13 其他经典推理方法114

5.14 找到更多的定理116

5.15 前推证明：转换定理117

5.15.1 使用of,where和THEN修改定理117

5.15.2 使用OF修正定理120

5.16 向后证明中的前向推理121

5.16.1 insert方法122

5.16.2 subgoal tac方法123

5.17 大型证明的管理125

5.17.1 策略或控制结构125

5.17.2 子目标编号126

5.18 证明欧几里德算法的正确性128

第六章 集合、函数和关系133

6.1 集合133

6.1.1 有限集的记号135

6.1.2 集合描述方法（set comprehension）136

6.1.3 绑定算子136

6.1.4 有限性和基数138

6.2 函数138

6.2.1 函数基础知识138

6.2.2 单射，满射，双射139

6.2.3 函数的像140

6.3 关系141

6.3.1 关系基础141

6.3.2 自反与传递闭包142

6.3.3 一个证明样本143

6.4 良基关系和归纳法144

6.5 不动点算子146

6.6 案例学习：模型检验的验证147

6.6.1 命题动态逻辑——PDL149

6.6.2 计算树逻辑——CTL152

第七章 集合递归定义160

7.1 偶数集合160

7.1.1 构造递归定义160

7.1.2 使用引入规则161

7.1.3 规则归纳法162

7.1.4 规则归纳法与推广163

7.1.5 规则反演164

7.1.6 交叉归纳定义166

7.1.7 归纳定义谓词167

7.2 自反传递闭包167

7.3 高级归纳定义171

7.3.1 引入规则中的全称量词171

7.3.2 使用单调函数的另一种定义173

7.3.3 等价性证明175

7.3.4 规则反演的另一例176

7.4 案例学习：上下文无关文法178

第三部分 高级材料187

第八章 高级types187

8.1 对和元组187

8.1.1 带元组的模式匹配187

8.1.2 定理证明188

8.2 记录191

8.2.1 记录基础知识191

8.2.2 可扩展记录和通用操作192

8.2.3 记录相等194

8.2.4 扩展和截断记录196

8.3 类型类（typeclasses）198

8.3.1 重载199

8.3.2 公理200

8.4 数205

8.4.1 数字文字206

8.4.2 自然数类型nat207

8.4.3 整数类型209

8.4.4 有理数、实数和复数211

8.4.5 数值类型类212

8.5 引入新类型215

8.5.1 声明新类型215

8.5.2 定义新类型216

第九章 高级化简与归纳220

9.1 化简220

9.1.1 高级特色220

9.1.2 化简器如何工作222

9.2 高级归纳技巧224

9.2.1 改造命题224

9.2.2 超结构归纳和超递归归纳226

9.2.3 新归纳格式的推导228

9.2.4 再访CTL229

第十章 案例学习：验证安全协议234

10.1 Needham-Schroeder公钥协议235

10.2 代理与消息237

10.3 敌方建模238

10.4 事件追踪240

10.5 协议建模241

10.6 证明基本性质243

10.7 证明安全性定理245

附录248

参考文献250

译后记254