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

定　價：￥59.00

作　者：	（德）伯托特，（德）卡斯特蘭著，顧明等譯
出版社：	清華大學(xué)出版社
叢編項：	國外經(jīng)典教材·計算機(jī)科學(xué)與技術(shù)
標(biāo)　簽：	程序設(shè)計

購買這本書可以去

ISBN：	9787302208136	出版時間：	2010-01-01	包裝：	平裝
開本：	大16開	頁數(shù)：	432	字?jǐn)?shù)：

內(nèi)容簡介

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

作者簡介

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

圖書目錄

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