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

　　Coq是一個用于驗證定理的證明是否正確的計算機工具?！谕评砗途幊谭矫?，Coq的語言都擁有足夠強大的能力和表達(dá)能力，可以構(gòu)造簡單的項，執(zhí)行簡單的證明，直到建了立完整的理論，學(xué)習(xí)復(fù)雜的算法。本書的主要目：標(biāo)是從實踐的角度來理解Coq系統(tǒng)及其基本理論。即歸納構(gòu)造演算。這本書給出了大量的例子，所有這些例子都可以在計算機上執(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ù)》作者簡介