交互式定理证明与程序开发：Coq归纳构造演算的艺术 - 国外经典教材·计算机科学与技术 - 中国高校教材图书网
| 内容简介： |
|
Coq 是一个用于验证定理的证明是否正确的计算机工具。这些定理可能涉及到普通数学、证明理论或程序验证。 我们的主要目标是从实践的角度来理解Coq 系统及其基本理论：归纳构造演算（the Calculus of Inductive Constructions）。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。我们也尽量分解对话（dialogues）以便读者能够通过纸笔或直接在Coq 上对其进行重现。有时，我们会给出一些综合表达式；它们乍看起来让人生畏，但事实上也是在Coq 证明辅助工具的帮助下得到的。读者应该在试验时对它们进行分解、修改、了解其结构，并获得一种实际的感受。 本书有一个相关网站1，读者可以从该网站下载并执行所有证明的例子。我们也提供了书中200 个练习的答案，以备不时之需。这本书及其网站使用的工具都是2004 年初发布的Coq V82。 用户对Coq 中已证明的定理的信心来自于构造演算（Calculus of Inductive Constructions）的性质。构造演算是一个形式系统。以λ 演算和类型（typing ）的观点来看，它结合了逻辑中的一些最新进展。这个演算的主要性质已在此处给出，因为我们相信结合理论和实践的知识是使用Coq 全部表达能力的一条最好的路径。
|
| 作者简介： |
|
|
| 章节目录： |
|
|
| 精彩片段： |
|
|
| 书 评： |
|
|
| 其 它： |
|
|
|
中国大学出版社协会 |
首页 |
宏观指导 |
出版社天地 |
图书代办站 |
教材图书信息 |
教材图书评论 |
在线订购 |
教材征订
