机器证明
机器证明的相关文献在1984年到2022年内共计112篇,主要集中在数学、自动化技术、计算机技术、科学、科学研究
等领域,其中期刊论文110篇、会议论文2篇、专利文献281174篇;相关期刊81种,包括瞭望、金色年华(教学参考)、湘潭师范学院学报(自然科学版)等;
相关会议2种,包括2017中国智能物联系统会议、2004年全国理论计算机科学学术年会等;机器证明的相关文献由112位作者贡献,包括刘保乾、张景中、李洪波等。
机器证明—发文量
专利文献>
论文:281174篇
占比:99.96%
总计:281286篇
机器证明
-研究学者
- 刘保乾
- 张景中
- 李洪波
- 郁文生
- 何灯
- 王渝生
- 付尧顺
- 侯晓荣
- 吴尽昭
- 吴文俊
- 杨路
- LiuWu
- Tianyu Sun
- Wensheng Yu
- Xiao-LinXiang
- Yong-BinLi
- 于尚超
- 付朝辉
- 何冠男
- 侯家利
- 关强
- 冯跃峰
- 刘佳
- 刘向晖
- 刘姜
- 别荣芳
- 印鉴
- 史璟
- 史继
- 吕红伟
- 吴忆平
- 周咸青
- 周海燕
- 唐云廷
- 夏兴国
- 夏壁灿
- 姜岩
- 孙凌云
- 孙天宇
- 小林英恒
- 左加亭
- 常剑迤
- 张奠宙
- 张家驹
- 张立先
- 彭翕成
- 徐嘉
- 戴望州
- 施齐焉
- 曾振柄
-
-
张景中;
赵维坤
-
-
摘要:
教育数学关注的是教材中数学内容的优化问题,就是要把数学变容易,从而真正减轻学生的学习负担。基于“熟悉了,简单了,想通了,直观了,就容易”的想法。把数学变容易的做法有:改变概念定义的表述;建立更简易、更有力的方法,提供解题的“中巧”。教育数学40多年的研究在五个方面有重要进展:在初等几何领域发展了面积法,进而发展出消点法;发现了三角函数在小学知识基础上的生长点;针对高中向量部分的学习,发展了向量回路方法;解决了有关微积分如何变容易的问题;探索如何将信息技术用于数学教学,开发了更智能化的动态数学软件--网络画板,使得数学教学更为生动有趣。
-
-
郭礼权;
付尧顺;
郁文生
-
-
摘要:
本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分没有极限的微积分理论构架的形式化验证,包括对张景中等发表的题为微积分基础的新视角"论文中全部定义和定理的Coq描述.进而,对定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.本文是实践研究人员利用计算机学习、理解、构建乃至教育现代数学理论的一个尝试.
-
-
曾振柄;
王建林;
杨争峰;
小林英恒
-
-
摘要:
本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
-
-
-
刘佳;
吕红伟;
付尧顺;
郁文生
-
-
摘要:
基于计算机证明辅助工具Coq,参考"公理化集合论"形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了Coq的规范、严谨、可靠.为构建完整的点集拓扑理论打下基础,在此系统下,有望实现拓扑空间相关性质的形式化系统.
-
-
-
-
-
摘要:
亚马逊是在几年前展开了零售团队的自动化,将预测需求、订购库存和谈判价格任务逐渐转移到了演算法上;在最初的时候,员工可以轻易的否决机器的决定,当厂商通知产品将要展开强势行销(marketingblitz)时,管理者便可以额外添加演算法并未预期的订单,然而随着机器证明了精确性,如今反而是人类员工必须为自己的更动辩护。
-
-
-
韩刚
-
-
摘要:
Based on the methods of historic analysis and literature research,this paper studies fourteen sets theorem’s created background,proof methods,and its popularization and application.The historical significance and influence of fourteen sets theorem on the mathematical development are discussed,and the prospect of this study is also described.%利用历史分析和文献考证的方法,对14集定理的产生背景、证明方法、推广应用进行整理研究,论述了其历史意义及对数学发展的影响,并且展望了该问题研究的前景。
-
-
-
Tianyu Sun;
孙天宇;
Wensheng Yu;
郁文生
- 《2017中国智能物联系统会议》
| 2017年
-
摘要:
利用交互式定理证明工具Coq,在公理化集合论体系下,给出选择公理与它的几个著名等价命题间等价性的机器证明,这些命题包括Tukey引理、Hausdorff最大原则、最大原则、Zorn引理、良序原则等.本文从选择公理出发依次证明上述定理,最后又通过良序原则证明了选择公理,从而循环证明了选择公理与这些命题间的等价性.本文体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.
-
-
-