內容簡介
Coq是一個用於驗證定理的證明是否正確的計算機工具。—在推理和編程方面,Coq的語言都擁有足夠強大的能力和表達能力,可以構造簡單的項,執行簡單的證明,直到建了立完整的理論,學習復雜的算法。
本書的主要目:標是從實踐的角度來理解Coq繫統及其基本理論。即歸納構造演算。這本書給出了大量的例子,所有這些例子都可以在計算機上執行。從本書配套網站WWW.labri.fr/Perso/~casteran/CoqArl可以下載並執行所有證明的例子,而且還提供了書中200個練習的答案。
這本書是一本很有價值的教材,它為初學者提供基礎訓練,為有經驗的人提供必要的專業知識,幫助學習者開發有實用價值的數學證明。
本書的主要目:標是從實踐的角度來理解Coq繫統及其基本理論。即歸納構造演算。這本書給出了大量的例子,所有這些例子都可以在計算機上執行。從本書配套網站WWW.labri.fr/Perso/~casteran/CoqArl可以下載並執行所有證明的例子,而且還提供了書中200個練習的答案。
這本書是一本很有價值的教材,它為初學者提供基礎訓練,為有經驗的人提供必要的專業知識,幫助學習者開發有實用價值的數學證明。