高阶逻辑辅助证明系统PDF电子书下载
- 电子书积分:11 积分如何计算积分?
- 作 者:(德)托比亚斯·尼普科夫(TobiasNipkow),(英)劳伦斯·鲍尔森(LawrenceC.Paulson),(德)玛尔库斯·温泽尔(MarkusWenzel)著
- 出 版 社:北京:北京理工大学出版社
- 出版年份:2013
- ISBN:9787564077631
- 页数:254 页
第一部分 基本技巧 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 tac 103
5.9.5 重用假设:frule 104
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 命题动态逻辑——PDL 149
6.6.2 计算树逻辑——CTL 152
第七章 集合递归定义 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
第八章 高级types 187
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 自然数类型nat 207
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 再访CTL 229
第十章 案例学习:验证安全协议 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
- 《管理信息系统习题集》郭晓军 2016
- 《信息系统安全技术管理策略 信息安全经济学视角》赵柳榕著 2020
- 《计算机辅助平面设计》吴轶博主编 2019
- 《程序逻辑及C语言编程》卢卫中,杨丽芳主编 2019
- 《系统解剖学速记》阿虎医考研究组编 2019
- 《慢性呼吸系统疾病物理治疗工作手册》(荷)瑞克·考斯林克(RikGosselink) 2020
- 《社会文化系统中的翻译》姜秋霞,杨正军 2019
- 《中国生态系统定位观测与研究数据集 森林生态系统卷 云南西双版纳》邓晓保·唐建维 2010
- 《大气氮沉降及其对生态系统的影响》方琨,王道波 2019
- 《庆祝新中国成立70周年当代中国发展的逻辑系列丛书 当代中国生态发展的逻辑》熊捷责编;包存宽 2020
- 《书情书》(德)布克哈德·施皮南(Burkhard Spinnen)著;(德)琳娜·霍文 2019
- 《手工咖啡 咖啡爱好者的完美冲煮指南》(美国)杰茜卡·伊斯托,安德烈亚斯·威尔霍夫 2019
- 《写给孩子的趣味天文学》(俄)雅科夫·伊西达洛维奇·别莱利曼著 2019
- 《美国的伤痕 独立战争与美国政治的暴力基因》(德)霍尔格·霍克(Holger Hoock)著 2019
- 《写给孩子的趣味物理学》(俄)雅科夫·伊西达洛维奇·别莱利曼著 2019
- 《文明的衰落与复兴》张娜责编;陈维政总主编;孙林译者;(德)阿尔伯特·史怀哲 2019
- 《厄特克尔家族》(德)鲁迪格·杨布鲁特著 2018
- 《弗里德里希·李斯特传》朱希滨责编;贾根良,梅俊杰总主编;梅俊杰译者;(德)欧根·文得乐 2019
- 《弗利克家族》(德)托马斯·拉姆什著 2018
- 《剑桥国际英语写作教程 从句子到段落》(美)劳里·布拉斯(Laurie Blass),(美)德德拉·戈登(Deborah Gordon)编著 2019
- 《大学计算机实验指导及习题解答》曹成志,宋长龙 2019
- 《指向核心素养 北京十一学校名师教学设计 英语 七年级 上 配人教版》周志英总主编 2019
- 《大学生心理健康与人生发展》王琳责任编辑;(中国)肖宇 2019
- 《大学英语四级考试全真试题 标准模拟 四级》汪开虎主编 2012
- 《大学英语教学的跨文化交际视角研究与创新发展》许丽云,刘枫,尚利明著 2020
- 《北京生态环境保护》《北京环境保护丛书》编委会编著 2018
- 《复旦大学新闻学院教授学术丛书 新闻实务随想录》刘海贵 2019
- 《大学英语综合教程 1》王佃春,骆敏主编 2015
- 《大学物理简明教程 下 第2版》施卫主编 2020
- 《指向核心素养 北京十一学校名师教学设计 英语 九年级 上 配人教版》周志英总主编 2019