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

　　數(shù)系的擴充始終貫穿于數(shù)學理論的發(fā)展之中.本書利用交互式定理證明工具Coq， 在Morse-Kelley 公理化集合論形式化系統(tǒng)下，給出中國科學與技術(shù)大學汪芳庭教授在其《數(shù)學基礎(chǔ)》中采用算術(shù)超濾分數(shù)構(gòu)造實數(shù)的機器證明系統(tǒng)， 包括超濾空間與算術(shù)超濾的基本概念、超濾變換以及用算術(shù)超濾構(gòu)造算術(shù)模型的形式化實現(xiàn)， 構(gòu)建了非標準實數(shù)模型， 自然包含標準實數(shù)模型， 并且給出濾子擴張原則和連續(xù)統(tǒng)假設蘊含非主算術(shù)超濾存在的形式化驗證. 在我們開發(fā)的系統(tǒng)中，全部定理無例外地給出Coq的機器證明代碼， 所有形式化過程已被Coq驗證， 并在計算機上運行通過， 充分體現(xiàn)了基于Coq 的數(shù)學定理機器證明具有可讀性、交互性和智能性的特點， 其證明過程規(guī)范、嚴謹、可靠. 該系統(tǒng)可方便地應用于非標準分析理論的形式化構(gòu)建.本書可作為數(shù)學與計算機科學、信息科學相關(guān)專業(yè)的高年級本科生或研究生教材， 也可供從事人工智能相關(guān)科研工作者學習參考.

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