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

定　價(jià)：￥59.00

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

購買這本書可以去

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

內(nèi)容簡(jiǎn)介

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

作者簡(jiǎn)介

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

圖書目錄

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