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

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

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