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

更多科學出版社服務，請掃碼獲取。