杭州电子科技大学图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

高阶逻辑辅助证明系统/(德)托比亚斯·尼普科夫(Tobias Nipkow)，(英)劳伦斯·鲍尔森(Lawrence C. Paulson)，(德)玛尔库斯·温泽尔(Markus Wenzel)著 陈光喜，刘卓军译

出版发行项:

北京:北京理工大学出版社,2013

ISBN及定价:

978-7-5640-7763-1 精装/CNY45.00

载体形态项:

253页;21cm

并列正题名:

Isabelle/HOL: a proof assistant for higher-order logic

个人责任者:

(德) 尼普科夫 (Nipkow, Tobias) 著

个人责任者:

(英) 鲍尔森 (Paulson, Lawrence C.) 著

个人责任者:

(德) 温泽尔 (Wenzel, Markus) 著

个人次要责任者:

陈光喜 译

个人次要责任者:

刘卓军 译

学科主题:

计算机辅助计算

中图法分类号:

TP391.75

版本附注:

经原作者和原出版社Springer Berlin Heidelberg授权出版

相关题名附注:

版权页英文题名：Isabelle/HOL: a proof assistant for higher-order logic

提要文摘附注:

本书是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论。本书分为三部分。第一部分是基本技巧：介绍在高阶逻辑中如何进行函数式程序建模，提供了表和自然数的简单证明实例。第二部分是逻辑与集合：介绍大量可供选择使用的低级证明策略。本部分描述了Isabelle/HOL如何处理集合、函数、关系以及如何实现递归定义集合，包括模型检验理论和经典教科书中关于形式语言的案例。第三部分是高级话题：包括实数、记录、重载技术等主题。本部分也讨论了归纳法和递归方法的高级技巧，还专门给出一章来介绍安全协议的形式化验证。

豆瓣简介：