可读证明

作品数：20被引量：61H指数：5
导出分析报告
相关领域：自动化与计算机技术理学更多>>
相关作者：郭远华张景中曾振柄陈世平刘忠更多>>
相关机构：中国科学院成都计算机应用研究所华东师范大学中国民航飞行学院广州大学更多>>
相关期刊：《计算机学报》《系统科学与数学》《计算机工程与设计》《中国学术期刊文摘》更多>>
相关基金：国家重点基础研究发展计划国家自然科学基金河南省科技攻关计划国家科技支撑计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
指数多项式不等式的自动证明被引量：3
《系统科学与数学》2017年第7期1692-1703,共12页陈世平 刘忠 
德阳市校(院;所)市科技合作计划资助课题
讨论了指数多项式不等式的自动证明问题,运用Taylor展开式将目标不等式的证明转化为一系列的一元多项式不等式的验证,然后借助代数不等式证明工具(如Bottema)完成最后的工作.运用Maple实现了上述算法,算法对所有指数多项式不等式终止,...
关键词：指数多项式不等式 自动证明 上限多项式 下限多项式 可读证明. 
Taylor展开式与三角函数不等式的自动证明被引量：6
《系统科学与数学》2016年第8期1339-1348,共10页陈世平 刘忠 
德阳市校(院;所)市科技合作计划资助课题
文章以具有模型f(x,tan(x/2))>0的三角函数不等式为研究对象来探讨超越不等式的机器证明问题,运用Taylor展开式将目标不等式的证明转化为一系列的一元多项式不等式的证明,然后借助代数不等式证明工具(如Bottema)完成最后的工作.运用Mapl...
关键词：超越不等式 三角函数不等式 机器证明 上限多项式 下限多项式 可读证明 
基于向量的几何可读自动证明被引量：2
《计算机学报》2014年第8期1809-1819,共11页葛强 张景中 陈矛 彭翕成 
国家自然科学基金(60903023;61304132);国家"八六三"高技术研究发展计划项目基金(2008AA01Z127);国家科技支撑计划课题(2013BAH18F02);河南省科技攻关计划项目(142102210397)资助~~
几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题...
关键词：机器证明 可读证明 前推法 向量 回路 
三角函数不等式的自动证明被引量：10
《四川大学学报（自然科学版）》2013年第3期537-540,共4页陈世平 
本文以三角函数不等式为研究对象来探讨超越不等式的机器证明问题,运用变量替换和函数的Taylor展开式将目标不等式代数化,然后借助BOTTEMA中强有力的代数不等式证明工具完成最后的证明.编制程序实现了上述算法,实验结果表明算法对常见...
关键词：超越不等式 三角函数不等式 自动证明 BOTTEMA 可读证明 
实轮换对称型及其半正定性判定的可读证明
《系统科学与数学》2012年第8期986-1001,共16页陈胜利 黄方剑 
中国科学院知识创新工程资助项目(KJCX-YW-S02)
可读证明是不等式机器证明领域中的热点问题.针对具有对称零点的实轮换对称型,文章提出了其线性空间的一组基以及分拆算法和两种分拆形式用于对不等式进行可读证明研究.讨论了该线性空间的维数,以及轮换对称型半正定性的判别方法.给出...
关键词：轮换对称型 对称零点 可读证明 半正定性判定 
一类三角形几何不等式的自动证明被引量：4
《计算机应用研究》2012年第5期1732-1736,共5页陈世平 刘忠 
讨论了一类只含三角函数的三角形几何不等式的自动证明问题。运用代数方法将其有理化,在不新增加根式的条件下将问题转换为一个二元多项式不等式的证明,设计的基于胞腔分解和实根分离的算法实现了二元多项式不等式的自动证明,输出的证...
关键词：几何不等式 可读证明 有理化 实根分离 胞腔分解 
启发式方法生成命题逻辑可读证明被引量：1
《计算机应用研究》2011年第12期4429-4432,共4页郭远华 
探讨了自动生成命题逻辑系统R的可读证明。采用试探法和自然推理法分别从前推和后推模拟人类思维求证,试探法根据推理规则将待证公式反向分解,自然推理法从假设出发根据推理规则生成新的公式。两种方法都实现了相干命题逻辑系统R的可读...
关键词：命题逻辑 启发式方法 试探法 自然推理法 可读证明 
相干命题逻辑自然推理系统NR的自动证明被引量：1
《计算机应用研究》2009年第10期3639-3641,共3页郭远华 曾振柄 
国家自然科学基金重点资助项目(90718041)
给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列。对系...
关键词：相干命题 自然推理 自动证明 可读证明 
重言衍推系统的试探法自动证明
《计算机应用与软件》2009年第9期34-37,45,共5页郭远华 曾振柄 
国家重点基础研究发展项目(2004CB318003);国家自然科学基金重点项目(90718041)
提出针对重言衍推系统的模仿人类思维方式的生成可读证明的算法:试探法。试探法将待证的命题逐步分解成子命题并构造一颗证明树,对重言衍推系统中的定理证明取得了较好的效果。
关键词：重言衍推 自动推理 可读证明 证明树 试探法 
几何定理机器证明三十年被引量：10
《系统科学与数学》2009年第9期1155-1168,共14页张景中 李永彬 
"973"(2004CB318000)项目资助
由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今30年,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值方法均能有效地判定其真假,面积法(消点法)、搜索...
关键词：几何定理机器证明 可读证明 代数方法 面积法 基于数据库的搜索法. 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部