本書利用交互式定理證明工具Coq，在樸素集合論的基礎上，從Peano五條公設出發(fā)，完整實現(xiàn)Landau有名的《分析基礎》中實數理論的形式化系統(tǒng)，包括對該專著中全部5個公設、73條定義和301個定理的Coq描述，其中依次構造了自然數、分數、分割、實數和復數，并建立了Dedekind實數完備性定理，從而迅速且自然地給出數學分析的堅實基礎。在分析基礎形式化系統(tǒng)下，給出Dedekind實數完備性定理與它的幾個有名等價命題間等價性的機器證明，這些命題包括確界存在定理、單調有界定理、Cauchy-Cantor閉區(qū)間套定理、Heine-Borel-Lebesgue有限覆蓋定理、Bolzano-Weierstrass聚點原理、Bolzano-Weierstrass列緊性定理及Bolzano-Cauchy收斂準則等，基于實數的完備性定理，作為應用，進一步給出閉區(qū)間上連續(xù)函數的重要性質——有界性定理、很值定理、介值定理、一致連續(xù)性定理——的機器證明。另外，還給出張景中院士提出的第三代微積分——不用極限的微積分——的形式化系統(tǒng)實現(xiàn)。在我們開發(fā)的系統(tǒng)中，全部定理無例外地給出Coq的機器證明代碼，所有形式化過程已被Coq驗證，并在計算機上運行通過，體現(xiàn)了基于Coq的數學定理機器證明具有可讀性和交互性的特點，其證明過程規(guī)范、嚴謹、可靠。該系統(tǒng)可方便地應用于數學分析相關理論的形式化構建。本書可作為數學與計算機科學、信息科學相關專業(yè)的高年級本科生或研究生教材，也可供從事人工智能相關科研工作者參考。
|
