书目详细信息
： 交互式定理证明与程序开发:Coq归纳构造演算的艺术
书目信息 机读格式(MARC)
| ISBN/价格： | 978-7-302-20813-6:CNY59.00 |
|---|---|
| 作品语种： | chi |
| 出版国别： | CN 110000 |
| 题名责任者项： | 交互式定理证明与程序开发/.(德) Yves Bertot, Pierre Casteran著/.顾明等译 |
| 出版发行项： | 北京:,清华大学出版社:,2010.1 |
| 载体形态项： | 19, 432页:;+26cm |
| 丛编项： | 国外经典教材.计算机科学与技术 |
| 提要文摘： | 本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。我们也尽量分解对话（dialogues）以便读者能够通过纸笔或直接在Coq 上对其进行重现。 |
| 题名主题： | 定理证明 软件工具 教材 |
| 非控主题词： | Coq |
| 中图分类： | O141-39 |
| 个人名称等同： | 伯托特 著 |
| 个人名称等同： | 卡斯特兰 著 |
| 个人名称次要： | 顾明 译 |