叶世伟

作品数：51被引量：259H指数：7
导出分析报告
供职机构：中国科学院计算技术研究所更多>>
发文主题：定理证明形式化流形学习形式化验证HOPFIELD网络更多>>
发文领域：自动化与计算机技术电子电信理学医药卫生更多>>
发文期刊：《计算机研究与发展》《软件学报》《计算机工程》《智能系统学报》更多>>
所获基金：国家自然科学基金中国科学院研究生院院长基金国际科技合作与交流专项项目北京市自然科学基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
串联机器人雅可比矩阵的高阶逻辑形式化被引量：4
《小型微型计算机系统》2016年第4期726-731,共6页杨秀梅 施智平 吴爱轩 关永 叶世伟 张杰 
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助;北京市优秀人才培养资助项目;北京市属高校青年拔尖人才培育计划资助
机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出100%精确和完备的分析与验证.基于高阶逻辑定理证明技术固有的高...
关键词：机器人雅可比矩阵 运动旋量 HOL4 形式化验证 
分数阶微积分定义的一致性在HOL4中的验证被引量：4
《计算机科学》2016年第3期23-26,53,共5页李姗姗 赵春娜 关永 施智平 王瑞 李晓娟 叶世伟 
国际科技合作计划项目(2010DFB10930;2011DFG13000);国家自然科学基金项目(60873006;61070049;61170304;61104035;61174145;61201378);北京市自然科学基金项目;北京市优秀人才项目(4122017;KZ201210028036;KM201010028021;2012D005016000011)资助
分数阶微积分有3种常用的定义:Grunwald-Letnikov定义、Riemann-Liouville定义以及Caputo定义,3种定义之间存在着一定的联系,在一定条件下,它们可以相互转换。首先在高阶逻辑定理证明器HOL4中使用实数、积分、极限、超越函数等定理建立...
关键词：分数阶微积分 定理证明 Caputo定义 一致性 
连续傅里叶变换基础理论的高阶逻辑形式化被引量：2
《计算机科学》2015年第4期31-36,共6页吕兴利 施智平 李晓娟 关永 叶世伟 张杰 
国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(60873006;61070049;61170304;61104035;61373034;61303014);北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028 036);北京市优秀人才培养项目;北京市属高校青年拔尖人才培育计划资助
连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用。利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相...
关键词：形式化方法 定理证明 连续傅里叶变换 HOL4 频率响应 
GJK算法的一种特殊情形的形式化验证和应用被引量：3
《小型微型计算机系统》2015年第2期365-369,共5页安育龙 施智平 叶世伟 李晓娟 张杰 魏洪兴 
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(60873006,61070049,61170304,61104035,61373034,61303014)资助;北京市自然科学基金暨北京市教委重点项目(4122017,KZ201210028036)资助;北京市优秀人才培养项目资助;北京市属高校青年拔尖人才培育计划资助
计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言...
关键词：形式化方法 算法验证 机器人规划 定理证明 HOL 
拉普拉斯变换微积分性质在HOL4中的形式化被引量：2
《小型微型计算机系统》2014年第9期2177-2181,共5页赵刚 赵春娜 关永 吕兴利 李晓娟 施智平 王瑞 叶世伟 
国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035;61174145;61201378)资助;北京市自然科学基金项目;北京市优秀人才项目(4122017;KZ201210028036;KM201010028021;2012D005016000011)资助
拉普拉斯变换是系统时域频域分析转换的基本工具,基于拉普拉斯变换的数值计算广泛用于信号传输的评估和重要安全系统的分析等,但是其存在计算不精确等问题.高阶逻辑定理证明是验证系统的一种严密的形式化方法.本文在高阶逻辑证明工具HOL...
关键词：拉普拉斯变换 形式化验证 定理证明 HOL4 微积分性质 
矩阵变换理论在HOL4中的形式化被引量：3
《计算机仿真》2014年第3期289-294,共6页康西楠 施智平 叶世伟 关永 
矩阵是数学中最重要的概念之一,欧氏空间上的变换理论是对涉及到矩阵的系统进行分析的基础。形式化验证中的定理证明方法基于数理逻辑,是确保系统设计正确的有力方法。使用高阶逻辑,在定理证明器HOL4中添加矩阵变换理论定理库,将会提高H...
关键词：形式化 定理证明 矩阵变换 豪斯霍尔德矩阵 
实数二项式系数在HOL4中的形式化被引量：1
《计算机科学》2014年第2期15-18,共4页师丽坤 赵春娜 关永 施智平 李晓娟 叶世伟 
国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(6087 3006;61070049;61170304;61104035;61174145;61201378);北京市自然科学基金;北京市优秀人才项目(4122017;KZ201210028036;KM2010 10028021;2012D005016000011)资助
定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系...
关键词：实数二项式系数 高阶逻辑 定理证明 HOL4 分数阶微积分 
基于肌电和惯性传感器数据融合的脑卒中患者上肢够物运动定量评估被引量：7
《中国康复医学杂志》2013年第7期632-637,647,共7页刘霏 谢斌 黄真 叶世伟 吴健康 王才丰 黄帅 
国家自然科学基金资助项目(81272166)
目的:探讨融合肌电和惯性传感数据的定量化脑卒中患者上肢运动评估方法的有效性。方法:实验联合使用微型惯性传感器和多通道肌电传感器,同步采集了20例脑卒中患者(患者组)和年龄匹配的10名老年人(健康组)的肌电及运动数据,融合这两种数...
关键词：微传感器人体运动捕获 肌电 上肢康复 
函数矩阵理论在HOL4中的形式化被引量：2
《小型微型计算机系统》2013年第3期654-658,共5页刘振科 施智平 关永 金声震 张杰 叶世伟 李晓娟 
国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035)资助;北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028036)资助;北京市优秀人才培养资助项目;计算机体系结构国家重点实验室开放课题
定理证明是重要的形式化验证方法之一,其将系统建模为逻辑公式,依托定理证明器进行推理从而完成验证.定理证明器中包含的定理库越多,其建模和推理能力越强.控制理论中经常用函数向量描述状态空间,形式化函数矩阵理论对控制系统的形式化...
关键词：函数矩阵 形式化验证 矩阵微分法 定理证明 HIGHER-ORDER Logic4 
Gauge积分在HOL4中的形式化被引量：7
《计算机科学》2013年第2期191-194,228,共5页谷伟卿 施智平 关永 张杰 赵春娜 叶世伟 
国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(61070049;61170304;61104035);北京市自然科学基金项目资助
积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4(Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分...
关键词：形式化验证 定理证明 Gauge积分 HOL4 积分器 
全选清除导出
共6页<123456>
检索报告 对象比较 聚类工具 使用帮助 返回顶部