自然數(shù)的緊化延伸機(jī)器證明系統(tǒng)

　　數(shù)系的擴(kuò)充始終貫穿于數(shù)學(xué)理論的發(fā)展之中.本書利用交互式定理證明工具Coq， 在Morse-Kelley 公理化集合論形式化系統(tǒng)下，給出中國科學(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)中，全部定理無例外地給出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)用于非標(biāo)準(zhǔn)分析理論的形式化構(gòu)建.本書可作為數(shù)學(xué)與計算機(jī)科學(xué)、信息科學(xué)相關(guān)專業(yè)的高年級本科生或研究生教材， 也可供從事人工智能相關(guān)科研工作者學(xué)習(xí)參考.

　　第三屆楊嘉墀科技獎（2013），吳文俊人工智能科學(xué)技術(shù)獎自然科學(xué)獎（2017）。