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

更多科學出版社服務，請掃碼獲取。