书目信息 |
| 题名： |
高阶逻辑辅助证明系统
|
|
| 作者： | 尼普科夫 ， 鲍尔森 ， 温泽尔 著 ；陈光喜 ， 刘卓军 译 | |
| 分册： | ||
| 出版信息： | 北京 北京理工大学出版社 2013 |
|
| 页数： | 253页 | |
| 开本： | 21cm | |
| 丛书名： | ||
| 单 册： | ||
| 中图分类： | O141.2 | |
| 科图分类： | ||
| 主题词： | 高阶--逻辑证明 , 高阶 , 逻辑证明 | |
| 电子资源： | ||
| ISBN： | 978-7-5640-7763-1 | |
| 000 | 01910nam0 2200337 450 | |
| 001 | 523 | |
| 005 | 20140910083548.39 | |
| 010 | @a978-7-5640-7763-1@b精装@dCNY45.00 | |
| 100 | @a20131104d2013 em y0chiy50 ea | |
| 101 | 1 | @achi@ceng |
| 102 | @aCN@b110000 | |
| 105 | @ay z 000yy | |
| 106 | @ar | |
| 200 | 1 | @a高阶逻辑辅助证明系统@AGao Jie Luo Ji Fu Zhu Zheng Ming Xi Tong@f(德)托比亚斯·尼普科夫(Tobias Nipkow)，(英)劳伦斯·鲍尔森(Lawrence C. Paulson)，(德)玛尔库斯·温泽尔(Markus Wenzel)著@F( De ) Tuo Bi Ya Si· Ni Pu Ke Fu (Tobias Nipkow)，( Ying ) Lao Lun Si· Bao Er Sen (Lawrence C. Paulson)，( De ) Ma Er Ku Si· Wen Ze Er (Markus Wenzel) Zhu@g陈光喜，刘卓军译 |
| 210 | @a北京@c北京理工大学出版社@d2013 | |
| 215 | @a253页@d21cm | |
| 305 | @a据本书原出版社“Springer Berlin Heidelberg”2002年版及其2011年电子版本、2012年电子版本译出 | |
| 312 | @a封面英文题名：A proof assistant for higher-order logic | |
| 330 | @a本书是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论。分为三部分，第一部分基本技巧：介绍在高阶逻辑中如何进行函数式程序建模，提供了表和自然数的简单证明实例；第二部分逻辑与集合：介绍大量可供选择使用的低级证明策略，描述了Isabelle/HOL如何处理集合、函数、关系以及如何实现递归定义集合，包括模型检验理论和经典教科书中关于形式语言的案例；第三部分高级话题：包括实数、记录、重载技术等主题，讨论了归纳法和递归方法的高级技巧，还专门介绍了安全协议的形式化验证。 | |
| 510 | 1 | @aProof assistant for higher-order logic@zeng |
| 606 | 0 | @a高阶@x逻辑证明 |
| 606 | 0 | @a高阶 |
| 606 | 0 | @a逻辑证明 |
| 690 | @aO141.2@v5 | |
| 701 | 0 | @c(德)@a尼普科夫@ANi Pu Ke Fu@c(Nipkow, Tobias)@4著 |
| 701 | 0 | @c(英)@a鲍尔森@ABao Er Sen@c(Paulson, Lawrence C.)@4著 |
| 701 | 0 | @c(德)@a温泽尔@AWen Ze Er@c(Wenzel, Markus)@4著 |
| 702 | 0 | @a陈光喜@AChen Guang Xi@f(1971~)@4译 |
| 702 | 0 | @a刘卓军@ALiu Zhuo Jun@4译 |
| 801 | 0 | @aCN@bTANGWEI@c20140603 |
| 905 | @b0839629-31@dO141.2@e97@f3 | |
| 高阶逻辑辅助证明系统/(德)托比亚斯·尼普科夫(Tobias Nipkow)，(英)劳伦斯·鲍尔森(Lawrence C. Paulson)，(德)玛尔库斯·温泽尔(Markus Wenzel)著/陈光喜，刘卓军译.-北京：北京理工大学出版社，2013 |
| 253页；21cm |
| ISBN 978-7-5640-7763-1(精装)：CNY45.00 |
| 本书是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论。分为三部分，第一部分基本技巧：介绍在高阶逻辑中如何进行函数式程序建模，提供了表和自然数的简单证明实例；第二部分逻辑与集合：介绍大量可供选择使用的低级证明策略，描述了Isabelle/HOL如何处理集合、函数、关系以及如何实现递归定义集合，包括模型检验理论和经典教科书中关于形式语言的案例；第三部分高级话题：包括实数、记录、重载技术等主题，讨论了归纳法和递归方法的高级技巧，还专门介绍了安全协议的形式化验证。 |
| ● |
| 相关链接 |
|
|
|
|
正题名：高阶逻辑辅助证明系统
索取号：O141.2/97
预约/预借
| 序号 | 登录号 | 条形码 | 馆藏地/架位号 | 状态 | 备注 |
| 1 | 0839629 | 208396298 | 第二样本阅览室/ [索取号:O141.2/97] | 在馆 | |
| 2 | 0839630 | 208396305 | 密集书库-数信学院/ [索取号:O141.2/97] | 在馆 | |
| 3 | 0839631 | 208396314 | 第三借阅区/ [索取号:O141.2/97] | 在馆 |