大拱桥--暨南大学学生门户 » 图书馆 » 算法理论 » 高阶逻辑辅助证明系统
名称 高阶逻辑辅助证明系统
索引号 TP301.6/20142
分类号 TP301.6
TP301.6(算法理论)
TP301(理论、方法)
TP30(一般性问题)
TP3(计算技术、计算机技术)
TP(自动化技术计算技术技术)
T(工业技术)
作者 尼普科夫、鲍尔森、温泽尔、陈光喜、刘卓军、
出版社 北京 : 北京理工大学出版社, 2013
ISBN 978-7-5640-7763-1
页数 253页 : 图 ; 21cm
价格 精装
标签
简介
注解 本书据2002年英文版译出 原文题名取自版权页 有书目 (第250-253页) 本书是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论。本书分为三部分。第一部分是基本技巧: 介绍在高阶逻辑中如何进行函数式程序建模, 提供了表和自然数的简单证明实例。第二部分是逻辑与集合: 介绍大量可供选择使用的低级证明策略。本部分描述了Isabelle/HOL如何处理集合、函数、关系以及如何实现递归定义集合, 包括模型检验理论和经典教科书中关于形式语言的案例。第三部分是高级话题: 包括实数、记录、重载技术等主题。本部分也讨论了归纳法和递归方法的高级技巧, 还专门给出一章来介绍安全协议的形式化验证。