全国大中专教材网络采选系统

推荐纸质教材推荐数字资源

一元微积分机器证明系统

定价：￥188.00

作者：郁文生等

出版时间：2026-06

出版社：科学出版社

以下为《一元微积分机器证明系统》的配套数字资源，这些资源在您购买图书后将免费附送给您：

关闭

基本信息评价

出版社：科学出版社
ISBN：9787030860330
版次：1版
开本：B5
出版时间：2026-06

作者简介

1995.9–1998.6，北京大学，控制理论，博士
1991.9–1994.6，四川大学，应用数学，硕士
1983.9-1987-6，伊犁师范大学，数学，学士2014.9-至今，北京邮电大学，电子工程学院，三级教授
2009.1-2014.9，华东师范大学，上海高可信重点计算实验室，三级教授
2009.10-2009.12，迪肯大学，电子工程学院，访问教授
2000.1-2001.3，墨尔本大学，电子工程学院，访问研究员
1998.6-2009.1，中国科学院，自动化研究所，研究员第三届杨嘉墀科技奖（2013），吴文俊人工智能科学技术奖自然科学奖（2017）。中国系统仿真学会智能物联系统建模与仿真专业委员会副主任委员、中国自动化学会控制理论专业委员会委员、中国人工智能学会智能空天系统专业委员会委员、中国人工智能学会自然计算与数字智能城市专业委员会委员等，中国仿真学会理事、北京市人工智能学会常务理事等《动力学与控制学报》杂志编委。

查看全部

内容简介

本书利用交互式定理证明工具Coq，在朴素集合论和初等数论及代数知识形式化系统下，以华东师范大学数学系编著的《数学分析》为基本构架，实现一元微积分的机器证明系统，包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、微分中值定理、实数的完备性、不定积分、定积分以及两个重要极限等内容的形式化实现。在我们开发的系统中，全部定理无一例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地应用于拓扑学和代数学理论的形式化构建，实现读者跟随计算机学习、理解、构建乃至发展现代数学的尝试，进一步提高认识数学、感受数学和欣赏数学的素养。
　　为方便应用和完整起见，附录中给出了Morse？Kelley公理集合论以及Zorich的著名著作《数学分析》中实数公理化形式系统的结构化表述。