西安工业大学图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

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

出版发行项:

北京:北京理工大学出版社,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) 著

个人次要责任者:

陈光喜 译

个人次要责任者:

刘卓军 译

学科主题:

电子计算机-逻辑运算

中图法分类号:

TP301.6

版本附注:

本书据2002年英文版译出

相关题名附注:

原文题名取自版权页

书目附注:

有书目 (第250-253页)

提要文摘附注:

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

豆瓣简介：