| 词条 | 交互式定理证明与程序开发 |
| 释义 | 图书信息交互式定理证明与程序开发 作 者： （德）伯托特，（德）卡斯特兰 著，顾明 等译 出 版 社： 清华大学出版社 出版时间： 2010-1-1 开 本： 大16开 I S B N ： 9787302208136 定价：￥59.00 内容简介Coq是一个用于验证定理的证明是否正确的计算机工具。—在推理和编程方面，Coq的语言都拥有足够强大的能力和表达能力，可以构造简单的项，执行简单的证明，直到建了立完整的理论，学习复杂的算法。 这本书是一本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。 目录1 概述 2 类型和表达式 3 命题和证明 4 依赖积 5 常用逻辑 6 归纳数据类型 7 证明策略和自动化证明 8 归纳谓词 9 函数及其规范 10 程序抽取和命令式程序设计 11 实例分析 12 模块系统 13 无穷对象和证明 14 归纳类型基础 15 一般递归 16 自反证明 附录 参考文献 |
| 随便看 |
百科全书收录4421916条中文百科知识，基本涵盖了大多数领域的百科知识，是一部内容开放、自由的电子版百科全书。