定理机器证明

作品数:55被引量:64H指数:4
导出分析报告
相关领域:自动化与计算机技术理学更多>>
相关作者:孙吉贵印鉴李莹朱兴军吴尽昭更多>>
相关机构:吉林大学中国科学院数学与系统科学研究院北京邮电大学华东师范大学更多>>
相关期刊:《系统科学与数学》《计算机技术与发展》《数学教学》《高等数学研究》更多>>
相关基金:国家自然科学基金吉林省青年科研基金中国博士后科学基金国家重点基础研究发展计划更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-10
视图:
排序:
基于Coq的两个重要极限的形式化证明
《中国科技论文在线精品论文》2021年第2期177-186,共10页赵保强 于畅 郁文生 
数学机械化主要是利用计算机实现对数学定理的推理,形式化数学是数学机械化的重要内容.本文利用交互式定理证明工具Coq实现两个重要极限的形式化证明,其中主要包括集合、数列、函数、极限等概念的定义以及相关定理的证明.在此基础上建...
关键词:人工智能 极限 形式化验证 定理机器证明 级数 COQ 
科技创新正在更新教学被引量:1
《科技导报》2020年第10期52-53,共2页林群 
现代科技,基于计算机强大的计算能力,发展了信息技术,包括手机、无线网络、视频、网课……甚至发展到人工智能(代替大脑)。它们正在改变我们的生活和工作,同时也改变了科学、工程学和社会学。以数学为例,出现了吴文俊的"数学定理机器证...
关键词:定理机器证明 人工智能 信息技术 张景中 计算能力 吴文俊 无线网络 创造性的工作 
C_m命题演算的定理机器证明系统
《辽宁大学学报(自然科学版)》2019年第1期31-37,共7页张伟 
辽宁省自然科学基金计划重点项目(20170540311);东北大学2017年本科教学质量工程项目(201755)
C_m系统是制约逻辑的命题演算系统,但是其推导定理的过程可否由图灵(计算机)算法完成尚未得到明确的结论.研究证明了C_m的公式集是递归可枚举集,并且给出了一个递归枚举算法,该算法能够对任一给定的实际可证的C_m式在有限的步骤内判定...
关键词:Cm系统 制约逻辑 可计算性 定理机器证明 
质点几何定理机器证明的研究进展
《应用数学进展》2018年第12期1490-1499,共10页胡晓璐 江建国 张媛 
质点几何定理机器证明是当前几何定理机器证明领域内的一个研究热点。本文介绍了质点几何的基本理论。综述了质点几何定理机器证明近年来取得的一些比较显著的进展。比较了质点法和质点消去法这两种证明方法的优缺点。最后,展望了这个...
关键词:自动推理 质点几何 质点法 质点消去法 
信念修正开放过程模式可判定公式表达能力被引量:1
《吉林大学学报(工学版)》2016年第6期2021-2026,共6页张伟 柳玉辉 
国家科技支撑计划项目(2014BAI17B01);软件开发环境国家重点实验室开放课题项目(SKLSDE-2012KF-02)
提出了一种可以在两个极大可判定前缀词公式类上实现信念修正OPEN过程模式的算法,该算法从初始形式理论出发,依据不断获取的新事实信息,迭代修正形式理论,完成形式理论的进化。探讨了OPEN过程模式的两种可判定公式类的表达能力,证明了...
关键词:人工智能 信念修正 开放过程模式 可判定公式类 表达能力 定理机器证明 
从解析的角度认识面积消点法
《数学教学》2016年第3期35-37,共3页徐章韬 赵晨 
方程是初中代数课程的核心,“以方程为纲,以元为序”可以对初中代数内容进行重建.几何是初中数学的另一支柱内容,根据已有的研究,用面积法可以对平面几何、三角等内容进行重构.上述思想,不仅可以指导课程内容的重构,还可以成为...
关键词:面积法 消点法 加减消元法 平面几何 解析 定理机器证明 课程内容 解方程 
天堑变通途——《初等几何研究(第2版)》代序
《高等数学研究》2015年第5期F0002-F0002,共1页陆汝钤 
由我国著名数学家吴文俊、张景中两位院士分别创建的两种几何定理机器证明,使我国在这一领域处于世界领先地位,正如王梓坤院士讲的,"我们可以自豪地说,几何定理机器证明研究的重大成果都是由我国数学家所取得的",可是,长期以来都以为行...
关键词:初等几何 定理机器证明 数学家 院士 吴文俊 
例谈平面几何问题的函数建模研究
《中学数学研究(华南师范大学)(下半月)》2015年第8期48-48,F0003,F0004,共3页张兴华 
"数无形,少直观,形无数,难入微",数形结合思想作为数学中非常重要的一种数学思想,是中学阶段学生必须培养的.初中,平面直角坐标系的引入为函数的学习作了准备,也为后续一次函数、反比例函数、二次函数为几何问题的函数建模提供了可能...
关键词:数形结合思想 平面直角坐标系 全等三角形 定理机器证明 已知条件 辅助线 坐标法 直观性 解形 极坐标系 
本体推理在几何定理机器证明中的应用
《计算机技术与发展》2013年第9期78-81,共4页李晓霞 陈强 
2012年广东省高等院校学科建设专项资金项目(2012KJCX0079);2011年东莞市现代信息服务业发展专项资金竞争性项目(DG201101)
文中阐述了平面几何定理机器证明的基本原理及方法,针对几何定理机器证明过程中可读证明的产生,及推理信息快速增长的问题,提出了一种基于本体推理的几何定理机器证明方法。通过具体案例,描述了以Protégér软件为工具,基于WordNet重用...
关键词:定理机器证明 本体模型 规则 推理 领域属性 
基于拼凑替换的定理机器证明的研究与实现
《计算机技术与发展》2012年第6期135-138,146,共5页于尚超 李阳 王鹏 
机器定理证明可以避免人工证明容易出现的低级错误,是人工智能的重要方面,有广泛的应用前景;函数式程序设计的设计思想更加接近于数学,在定理证明方面有天然优势。人们证明逻辑推理的过程通过函数式程序实现,并将其证明的步骤显示出来,...
关键词:机器证明 人工智能 自动推理 
检索报告 对象比较 聚类工具 使用帮助 返回顶部