-
Title
题名
交互式定理证明与程序开发：Ｃｏｑ归纳构造演算的艺术 -
Publication Information
出版信息
Tsinghua University Press
清华大学出版社 -
Publication Type
文献类型
图书/专著 -
Publication Year
出版时间
2010 -
Publisher
出版单位
Tsinghua University Press
清华大学出版社 -
Place of Publication
出版地
China
中国 -
Language
语言
Simplified Chinese
中文简体 -
ISBN
ISBN
9787302208136 -
Series
丛书
国外经典教材·计算机科学与技术 -
Research Topics
研究主题
-
Abstract
摘要
目录
1 概述
2 类型和表达式
3 命题和证明
4 依赖积
5 常用逻辑
6 归纳数据类型
7 证明策略和自动化证明
8 归纳谓词
9 函数及其规范
10 程序抽取和命令式程序设计
11 实例分析
12 模块系统
13 无穷对象和证明
14 归纳类型基础
15 一般递归
16 自反证明
附录
参考文献内容简介
《交互式定理证明与程序开发：Coq归纳构造演算的艺术》的主要目标是从实践的角度来理解Coq系统及其基本理论，即归纳构造演算。这《交互式定理证明与程序开发：Coq归纳构造演算的艺术》给出了大量的例子，所有例子都町以在计算机上执行。从《交互式定理证明与程序开发：Coq归纳构造演算的艺术》配套网站可以下载并执行所有证明的例子，而且还提供了书中200个练习的答案。
Coq是一个用于验证定理的证明是否正确的计算机工具。在推理和编程方面，Coq的语言都拥有足够强大的能力和表达能力，可以构造简单的项，执行简单的证明，直到建立完整的理论，学习复杂的算法。
这《交互式定理证明与程序开发：Coq归纳构造演算的艺术》是·本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。
-
Full Text/Access
全文链接