交互式定理證明與程序開發(fā)：Coq歸納構造演算的藝術

定　價：￥59.00

作　者：	（德）伯托特，（德）卡斯特蘭著，顧明等譯
出版社：	清華大學出版社
叢編項：	國外經典教材·計算機科學與技術
標　簽：	程序設計

購買這本書可以去

ISBN：	9787302208136	出版時間：	2010-01-01	包裝：	平裝
開本：	大16開	頁數：	432	字數：

內容簡介

　　Coq是一個用于驗證定理的證明是否正確的計算機工具?！谕评砗途幊谭矫?，Coq的語言都擁有足夠強大的能力和表達能力，可以構造簡單的項，執(zhí)行簡單的證明，直到建了立完整的理論，學習復雜的算法。本書的主要目：標是從實踐的角度來理解Coq系統及其基本理論。即歸納構造演算。這本書給出了大量的例子，所有這些例子都可以在計算機上執(zhí)行。從本書配套網站WWW.labri．fr／Perso／～casteran／CoqArl可以下載并執(zhí)行所有證明的例子，而且還提供了書中200個練習的答案。這本書是一本很有價值的教材，它為初學者提供基礎訓練，為有經驗的人提供必要的專業(yè)知識，幫助學習者開發(fā)有實用價值的數學證明。

作者簡介

暫缺《交互式定理證明與程序開發(fā)：Coq歸納構造演算的藝術》作者簡介

圖書目錄

1　概述
2　類型和表達式
3　命題和證明
4　依賴積
5　常用邏輯
6　歸納數據類型
7　證明策略和自動化證明
8　歸納謂詞
9　函數及其規(guī)范
10　程序抽取和命令式程序設計
11　實例分析
12　模塊系統
13　無窮對象和證明
14　歸納類型基礎
15　一般遞歸
16　自反證明
附錄
參考文獻