數(shù)系的擴(kuò)充始終貫穿于數(shù)學(xué)理論的發(fā)展之中. 本書利用交互式定理證明工具Coq, 在Morse-Kelley 公理化集合論形式化系統(tǒng)下, 給出中國(guó)科學(xué)與技術(shù)大學(xué)汪芳庭教授在其《數(shù)學(xué)基礎(chǔ)》中采用算術(shù)超濾分?jǐn)?shù)構(gòu)造實(shí)數(shù)的機(jī)器證明系統(tǒng), 包括超濾空間與算術(shù)超濾的基本概念、超濾變換以及用算術(shù)超濾構(gòu)造算術(shù)模型的形式化實(shí)現(xiàn), 構(gòu)建了非標(biāo)準(zhǔn)實(shí)數(shù)模型, 自然包含標(biāo)準(zhǔn)實(shí)數(shù)模型, 并且給出濾子擴(kuò)張?jiān)瓌t和連續(xù)統(tǒng)假設(shè)蘊(yùn)含非主算術(shù)超濾存在的形式化驗(yàn)證. 在我們開發(fā)的系統(tǒng)中, 全部定理無(wú)例外地給出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)用于非標(biāo)準(zhǔn)分析理論的形式化構(gòu)建. 本書可作為數(shù)學(xué)與計(jì)算機(jī)科學(xué)、信息科學(xué)相關(guān)專業(yè)的高年級(jí)本科生或研究生教材, 也可供從事人工智能相關(guān)科研工作者學(xué)習(xí)參考.

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