交互式定理证明与程序开发

图书信息交互式定理证明与程序开发

[1]

作者： （德）伯托特，（德）卡斯特兰著，顾明等译

出 版 社： 清华大学出版社

出版时间： 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自反证明

附录

参考文献