请输入您要查询的百科知识:

 

词条 交互式定理证明与程序开发
释义

图书信息

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

作 者: (德)伯托特,(德)卡斯特兰 著,顾明 等译

出 版 社: 清华大学出版社

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

附录

参考文献

随便看

 

百科全书收录4421916条中文百科知识,基本涵盖了大多数领域的百科知识,是一部内容开放、自由的电子版百科全书。

 

Copyright © 2004-2023 Cnenc.net All Rights Reserved
更新时间:2025/3/4 20:29:17