| ISBN/价格： | 978-7-5640-7763-1:CNY45.00 |
|---|
| 作品语种： | chi eng |
|---|
| 出版国别： | CN 110000 |
|---|
| 题名责任者项： | 高阶逻辑辅助证明系统/.(德) 托比亚斯·尼普科夫(Tobias Nipkow), (英) 劳伦斯·鲍尔森(Lawrence C.Paulson), (德) 玛尔库斯·温泽尔(MarkusWenzel)著/.陈光喜, 刘卓军译 |
|---|
| 出版发行项： | 北京:,北京理工大学出版社:,2013.5 |
|---|
| 载体形态项： | 253页:;+21cm |
|---|
| 相关题名附注： | 封面英文题名：A proof assistant for higher-order logic |
|---|
| 提要文摘： | 本书是在高阶逻辑中使用Isabelle辅助证明系统进行交互式证明的导论。分为三部分，第一部分基本技巧：介绍在高阶逻辑中如何进行函数式程序建模，提供了表和自然数的简单证明实例；第二部分逻辑与集合：介绍大量可供选择使用的低级证明策略，描述了Isabelle/HOL如何处理集合、函数、关系以及如何实现递归定义集合，包括模型检验理论和经典教科书中关于形式语言的案例；第三部分高级话题：包括实数、记录、重载技术等主题，讨论了归纳法和递归方法的高级技巧，还专门介绍了安全协议的形式化验证。 |
|---|
| 并列题名： | Proof assistant for higher-order logic eng |
|---|
| 题名主题： | 高阶 逻辑证明 |
|---|
| 中图分类： | O141.2 |
|---|
| 个人名称等同： | 尼普科夫 托比亚斯 著 |
|---|
| 个人名称等同： | 鲍尔森 劳伦斯 著 |
|---|
| 个人名称等同： | 温泽尔 玛尔库斯 著 |
|---|
| 个人名称次要： | 陈光喜 译 |
|---|
| 个人名称次要： | 刘卓军 译 |
|---|
| 记录来源： | CN LCTBU 20131104 |
|---|