交互式定理证明与程序开发：Coq归纳构造演算的艺术

定　价：¥59.00

作　者：	（德）伯托特，（德）卡斯特兰著，顾明等译
出版社：	清华大学出版社
丛编项：	国外经典教材·计算机科学与技术
标　签：	程序设计

购买这本书可以去

ISBN：	9787302208136	出版时间：	2010-01-01	包装：	平装
开本：	大16开	页数：	432	字数：

内容简介

　　Coq是一个用于验证定理的证明是否正确的计算机工具。—在推理和编程方面，Coq的语言都拥有足够强大的能力和表达能力，可以构造简单的项，执行简单的证明，直到建了立完整的理论，学习复杂的算法。本书的主要目：标是从实践的角度来理解Coq系统及其基本理论。即归纳构造演算。这本书给出了大量的例子，所有这些例子都可以在计算机上执行。从本书配套网站WWW.labri．fr／Perso／～casteran／CoqArl可以下载并执行所有证明的例子，而且还提供了书中200个练习的答案。这本书是一本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。