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