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

更多科學(xué)出版社服務(wù)，請掃碼獲取。