高阶逻辑辅助证明系统

图书标准信息

• 作者 [德]托比亚斯·尼普科夫、[英]劳伦斯·鲍尔森、[德]玛尔库斯·温泽尔 著；陈光喜、刘卓军 译
• 出版社 北京理工大学出版社
• 出版时间 2013-05
• 版次 1
• ISBN 9787564077631
• 定价 45.00元
• 装帧 精装
• 开本 32开
• 纸张 胶版纸
• 页数 253页
• 正文语种 简体中文

【内容简介】

　　《高阶逻辑辅助证明系统》是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论，适用于Isabelle系统的潜在使用者，自成体系，分为三部分：第一部分是基本技巧：介绍在高阶逻辑中如何进行函数式程序建模，提供了表（1ist）和自然数的简单证明实例。大多数证明只要两步完成：对所选变量进行归纳以及使用自动策略（auto）。当然，这些粗浅的例子仍然涵盖了嵌套递归和交叉递归等技术。第二部分是逻辑与集合：介绍大量可供选择使用的低级证明策略。
　　《高阶逻辑辅助证明系统》描述了Isabelle／HOL如何处理集合、函数、关系以及如何实现递归定义集合，包括模型检验理论和经典教科书中关于形式语言的案例。第三部分是高级话题：包括实数、记录、重载技术等主题。
　　《高阶逻辑辅助证明系统》也讨论了归纳法和递归方法的高级技巧，还专门给出一章来介绍安全协议的形式化验证。

【目录】

第一部分基本技巧
第一章基础
1.1引言
1.2theory（理论）
1.3类型，项和公式
1.4变元
1.5交互与界面
1.6启动
第二章HOL中的函数编程
第三章高级函数式编程
第四章theory的表示

第二部分逻辑与集合
第五章游戏规则
第六章集合、函数和关系
第七章集合递归定义
第八章高级types
第九章高级化简与归纳
第十章案例学习：验证安全协议
附录
参考文献
译后记一