MARC状态：审校 文献类型：中文图书 浏览次数：72
- 题名/责任者:
- 高阶逻辑辅助证明系统/(德) 托比亚斯·尼普科夫, (英) 劳伦斯·鲍尔森, (德) 玛尔库斯·温泽尔著 陈光喜, 刘卓军译
- 出版发行项:
- 北京:北京理工大学出版社,2013
- ISBN及定价:
- 978-7-5640-7763-1 精装/CNY45.00
- 载体形态项:
- 253页:图;21cm
- 个人责任者:
- 尼普科夫 (Nipkow, Tobias) 著
- 个人责任者:
- 鲍尔森 (Paulson, Lawrence C.) 著
- 个人责任者:
- 温泽尔 (Wenzel, Markus) 著
- 个人次要责任者:
- 陈光喜 译
- 个人次要责任者:
- 刘卓军 译
- 学科主题:
- 计算机辅助计算
- 中图法分类号:
- TP391.75
- 版本附注:
- 本书据2002年英文版译出
- 相关题名附注:
- 英文题名取自版权页
- 书目附注:
- 有书目 (第250-253页)
- 提要文摘附注:
- 本书是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论。本书分为三部分。第一部分是基本技巧: 介绍在高阶逻辑中如何进行函数式程序建模, 提供了表和自然数的简单证明实例。第二部分是逻辑与集合: 介绍大量可供选择使用的低级证明策略。本部分描述了Isabelle/HOL如何处理集合、函数、关系以及如何实现递归定义集合, 包括模型检验理论和经典教科书中关于形式语言的案例。第三部分是高级话题: 包括实数、记录、重载技术等主题。本部分也讨论了归纳法和递归方法的高级技巧, 还专门给出一章来介绍安全协议的形式化验证。
全部MARC细节信息>>
9楼北计算机应用借阅室