交互式定理证明与程序开发
交互式定理证明与程序开发
图书信息
交互式定理证明与程序开发
作 者: (德)伯托特,(德)卡斯特兰 著,顾明 等译
出 版 社: 清华大学出版社
出版时间: 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 自反证明
附录
参考文献