机器证明

作品数：221被引量：322H指数：10
导出分析报告
相关领域：理学自动化与计算机技术更多>>
相关作者：张景中杨路李洪波钟小梅徐扬更多>>
相关机构：中国科学院数学与系统科学研究院北京邮电大学中国科学院成都计算机应用研究所中国科学院更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划国家高技术研究发展计划中国科学院知识创新工程重要方向项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
中国数学家与机器证明
《中学生数学》2025年第5期19-20,共2页叶文明 李阳 
在浩瀚的数学宇宙中,中国数学家如同勇敢的探险家,以其独特的智慧和不懈的努力,不断开拓着新的领域.其中,机器证明作为数学与计算机科学交叉融合的前沿阵地,见证了中国数学家在这一领域的卓越成就.机器证明,这一数学与计算机科学跨界融...
关键词：智慧火花 计算机科学 机器证明 几何定理 数学命题 跨界融合 交叉融合 数学与计算机 
马库恩 用机器证明数学猜想
《环球人物》2024年第24期96-97,共2页尼克 
机器定理证明是人工智能中最古老也最困难的研究领域。在这一领域,威廉·马库恩(1953-2011)可以称得上是最杰出的实干家,他创立的一阶定理证明器Otter是上世纪90年代基于逻辑的定理证明器的集大成者,影响了当时整个定理证明领域的理论...
关键词：定理证明器 数学猜想 人工智能 机器证明 实验室 库恩 实干家 
不等式的非负分拆新探
《汕头大学学报（自然科学版）》2023年第4期20-32,共13页刘保乾 
应用符号运算软件Maple的多项式运算命令quo和rem,结合随机数验证程序,提出了一种不等式的非负分拆方法;通过大量的实例给出了这个非负分拆方法在证明三角形几何不等式和代数不等式方面的应用.提出了一个n元不等式问题.
关键词：不等式 非负分拆 随机数验证程序 机器证明 
把数学变容易--张景中院士访谈录被引量：6
《教育研究与评论》2022年第9期4-11,共8页张景中 赵维坤 
教育数学关注的是教材中数学内容的优化问题,就是要把数学变容易,从而真正减轻学生的学习负担。基于“熟悉了,简单了,想通了,直观了,就容易”的想法。把数学变容易的做法有:改变概念定义的表述;建立更简易、更有力的方法,提供解题的“...
关键词：教育数学 解题教学 机器证明 网络画板 
计算机能学会算计吗
《中国统计》2021年第9期47-49,共3页黄向阳 
计算已机械化了,证明还没有机械化。当然,证明和计算之间,并没有一条不可逾越的鸿沟:--吴文俊《王者之路--机器证明及其应用》本期居然会一头扎进我向来敬而远之的领域,对硅基智能体(人工智能)进行带有哲学意味的讨论,完全是意外的惊吓...
关键词：人工智能 智能体 计算机 哲学意味 机器证明 吴文俊 咬文嚼字 运气 
组合恒等式证明的几种方法
《理论数学》2021年第6期1137-1145,共9页郑欢欢 靳海涛 
通过含有二项式系数的一些恒等式,介绍了组合证明法、积分法、差分法、生成函数法和机器证明法五种常用的恒等式的证明方法。
关键词：二项式系数 组合恒等式 生成函数 机器证明 
基于Coq的两个重要极限的形式化证明
《中国科技论文在线精品论文》2021年第2期177-186,共10页赵保强 于畅 郁文生 
数学机械化主要是利用计算机实现对数学定理的推理,形式化数学是数学机械化的重要内容.本文利用交互式定理证明工具Coq实现两个重要极限的形式化证明,其中主要包括集合、数列、函数、极限等概念的定义以及相关定理的证明.在此基础上建...
关键词：人工智能 极限 形式化验证 定理机器证明 级数 COQ 
基于Coq的第三代微积分机器证明系统被引量：3
《中国科学：数学》2021年第1期115-136,共22页郭礼权 付尧顺 郁文生 
国家自然科学基金(批准号:61936008和61571064)资助项目。
本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分|没有极限的微积分|理论构架的形式化验证,包括对张景中等发表的题为\微积分基础的新视角"论文中全部定义和定理的Coq描述.进而,对定理无例外地给出Coq的机...
关键词：证明辅助工具Coq 第三代微积分 形式化 机器证明 
点集拓扑学之杨忠道定理的一个机械化证明被引量：1
《中国科学：数学》2021年第1期257-288,共32页曾振柄 王建林 杨争峰 小林英恒 
国家自然科学基金(批准号:11471209和61772203)资助项目。
本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
关键词：拓扑空间 开集 闭集 导集 杨忠道定理 机器证明 
基于Coq的有标集族相关定理的机器证明
《伊犁师范学院学报（自然科学版）》2020年第2期13-22,共10页刘佳 吕红伟 付尧顺 郁文生 
新疆维吾尔自治区自然科学基金项目(2018D01C008).
基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,...
关键词：COQ 机器证明 公理化集合论 有标集族 
全选清除导出
共22页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部