机读格式显示(MARC)

• 000 01706nam0 2200349 450

• 001 0000489881

• 005 20140115105100.0

• 010 __ |a 978-7-5640-7763-1 |b 精装 |d CNY45.00

• 099 __ |a CAL 012013127808

• 100 __ |a 20131030d2013 em y0chiy50 ea

• 101 1_ |a chi |c eng

• 102 __ |a CN |b 110000

• 105 __ |a ak a 000yy

• 106 __ |a r

• 200 1_ |a 高阶逻辑辅助证明系统 |A gao jie luo ji fu zhu zheng ming xi tong |f (德) 托比亚斯·尼普科夫, (英) 劳伦斯·鲍尔森, (德) 玛尔库斯·温泽尔著 |g 陈光喜, 刘卓军译

• 210 __ |a 北京 |c 北京理工大学出版社 |d 2013

• 215 __ |a 253页 |c 图 |d 21cm

• 305 __ |a 本书据2002年英文版译出

• 312 __ |a 英文题名取自版权页

• 320 __ |a 有书目 (第250-253页)

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

• 500 10 |a Isabelle/HOL : a proof assistant for higher-order logic |m Chinese

• 606 0_ |a 计算机辅助计算 |A ji suan ji fu zhu ji suan

• 690 __ |a TP391.75 |v 5

• 701 _1 |a 尼普科夫 |A ni pu ke fu |g (Nipkow, Tobias) |4 著

• 701 _1 |a 鲍尔森 |A bao er sen |g (Paulson, Lawrence C.) |4 著

• 701 _1 |a 温泽尔 |A wen ze er |g (Wenzel, Markus) |4 著

• 702 _0 |a 陈光喜 |A chen guang xi |4 译

• 702 _0 |a 刘卓军 |A liu zhuo jun |4 译

• 801 _0 |a CN |b WHUTL |c 20131102

• 905 __ |a SCNU |f TP391.75/8430

• 920 __ |a 242430 |z 1