本書利用交互式定理證明工具Coq，在樸素集合論的基礎(chǔ)上，從Peano五條公設(shè)出發(fā)，完整實(shí)現(xiàn)Landau有名的《分析基礎(chǔ)》中實(shí)數(shù)理論的形式化系統(tǒng)，包括對該專著中全部5個(gè)公設(shè)、73條定義和301個(gè)定理的Coq描述，其中依次構(gòu)造了自然數(shù)、分?jǐn)?shù)、分割、實(shí)數(shù)和復(fù)數(shù)，并建立了Dedekind實(shí)數(shù)完備性定理，從而迅速且自然地給出數(shù)學(xué)分析的堅(jiān)實(shí)基礎(chǔ)。在分析基礎(chǔ)形式化系統(tǒng)下，給出Dedekind實(shí)數(shù)完備性定理與它的幾個(gè)有名等價(jià)命題間等價(jià)性的機(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ì)算機(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)建。本書可作為數(shù)學(xué)與計(jì)算機(jī)科學(xué)、信息科學(xué)相關(guān)專業(yè)的高年級本科生或研究生教材，也可供從事人工智能相關(guān)科研工作者參考。
|
