| ISBN/价格： | 978-7-302-20813-6:CNY59.00 |
|---|
| 作品语种： | chi eng |
|---|
| 出版国别： | CN 110000 |
|---|
| 题名责任者项： | 交互式定理证明与程序开发/.(德)Yves Bertot，(德)Pierre Casteran著/.顾明等译 |
|---|
| 出版发行项： | 北京:,清华大学出版社:,2010.1 |
|---|
| 载体形态项： | 19,432页:;+26cm |
|---|
| 一般附注： | 国外经典教材·计算机科学与技术 |
|---|
| 提要文摘： | 本书的主要目标是从实践的角度来理解Coq系统及其基本理论：归纳构造演算。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。 |
|---|
| 并列题名： | Interactive theorem proving and program development : Coq’art: the calculus of inductive constructions eng |
|---|
| 题名主题： | 定理证明 软件工具 教材 |
|---|
| 中图分类： | O141-39 |
|---|
| 个人名称等同： | Bertot Yves 著 |
|---|
| 个人名称等同： | Casteran Pierre 著 |
|---|
| 个人名称次要： | 顾明 译 |
|---|
| 记录来源： | CN LCTBU 20101009 |
|---|