赵春娜

作品数：19被引量：261H指数：6
导出分析报告
供职机构：首都师范大学信息工程学院更多>>
发文主题：分数阶微积分定理证明分数阶系统形式化验证形式化更多>>
发文领域：自动化与计算机技术经济管理冶金工程兵器科学与技术更多>>
发文期刊：《宇航学报》《兵工学报》《系统仿真学报》《数学的实践与认识》更多>>
所获基金：国家自然科学基金北京市自然科学基金国际科技合作与交流专项项目北京市优秀人才培养资助更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
分数阶微积分定义的一致性在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定义 一致性 
拉普拉斯变换微积分性质在HOL4中的形式化被引量：2
《小型微型计算机系统》2014年第9期2177-2181,共5页赵刚 赵春娜 关永 吕兴利 李晓娟 施智平 王瑞 叶世伟 
国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035;61174145;61201378)资助;北京市自然科学基金项目;北京市优秀人才项目(4122017;KZ201210028036;KM201010028021;2012D005016000011)资助
拉普拉斯变换是系统时域频域分析转换的基本工具,基于拉普拉斯变换的数值计算广泛用于信号传输的评估和重要安全系统的分析等,但是其存在计算不精确等问题.高阶逻辑定理证明是验证系统的一种严密的形式化方法.本文在高阶逻辑证明工具HOL...
关键词：拉普拉斯变换 形式化验证 定理证明 HOL4 微积分性质 
实数二项式系数在HOL4中的形式化被引量：1
《计算机科学》2014年第2期15-18,共4页师丽坤 赵春娜 关永 施智平 李晓娟 叶世伟 
国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(6087 3006;61070049;61170304;61104035;61174145;61201378);北京市自然科学基金;北京市优秀人才项目(4122017;KZ201210028036;KM2010 10028021;2012D005016000011)资助
定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系...
关键词：实数二项式系数 高阶逻辑 定理证明 HOL4 分数阶微积分 
SpaceWire译码电路在HOL4中的形式化验证被引量：5
《小型微型计算机系统》2013年第8期1959-1963,共5页张玉鹏 施智平 关永 李黎明 赵春娜 张杰 
国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035)资助;北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028036)资助;北京市优秀人才培养项目资助
SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成...
关键词：SpaceWire标准 形式化验证 定理证明 HOL 
原料场智能逻辑控制系统被引量：3
《烧结球团》2013年第2期56-59,共4页袁晓红 赵明 赵春娜 
国家自然科学基金(项目批准号:61104035)
以唐钢原料场为例,介绍了大型原料场的工艺流程和控制方式,对常用的控制模式和实现方法进行了详细论述,介绍了控制系统的架构和硬件、软件设计。将工业现场总线技术和工业以太网技术结合,应用到大型综合原料场控制系统,解决了远程、强...
关键词：原料场 控制模式 可编程控制器 现场总线 工业以太网 
Gauge积分在HOL4中的形式化被引量：7
《计算机科学》2013年第2期191-194,228,共5页谷伟卿 施智平 关永 张杰 赵春娜 叶世伟 
国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(61070049;61170304;61104035);北京市自然科学基金项目资助
积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4(Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分...
关键词：形式化验证 定理证明 Gauge积分 HOL4 积分器 
多标志齐次变换的增强现实技术与虚拟教育应用被引量：1
《北京师范大学学报（自然科学版）》2013年第1期29-33,共5页谭小慧 周明全 樊亚春 范鹏程 赵春娜 
国家自然科学基金资助项目(61104035;61170203)
增强现实可实现真实场景与计算机虚拟信息的融合.研究了基于标志的增强现实技术,采用齐次变换实现基于标志的增强现实三维注册关键技术,改进了坐标齐次变换支持多标志识别,可同时对多个三维虚拟模型进行平移、旋转、缩放的刚体变换,实...
关键词：增强现实 齐次变换 虚拟现实教学 计算机视觉 
烧结系统终点温度与点火强度最优控制算法被引量：1
《烧结球团》2012年第5期12-15,共4页袁晓红 赵国新 赵春娜 
国家自然科学基金(项目批准号:61104035)
铁矿石烧结是钢铁生产流程的关键环节,烧结矿的物理特性,如强度、粉末含量、粒度,以及化学成分的稳定性直接影响高炉的炉况及铁水质量。通过最优控制算法,建立了烧结过程工艺参数与烧结终点温度之间的最优控制模型,实现了烧结终点温度...
关键词：烧结终点 温度 模型 最优算法 智能控制 
基于理想灰关联距离的课程评估方法被引量：4
《数学的实践与认识》2012年第2期27-35,共9页赵春娜 骆力明 石长地 赵雨 李英顺 
国家自然科学基金(61104035);北京市教委科技基金(KM201010028021);辽宁省自然科学基金(20062036;20082044)
综合灰色系统理论、理想解法和欧氏距离,提出了一种新的基于理想关联距离度的课程评估方法,给出了建立评估模型的基本步骤.定量处理的指标,经过理想化、标准化后,定义关联数,由此计算关联距离度.通过灰色关联距离度,建立了一种接近最优...
关键词：课程评估 理想解 灰关联分析 欧氏距离 
一种反辐射武器作战效能评估方法被引量：15
《兵工学报》2011年第3期321-326,共6页刘义 赵春娜 王雪松 王国玉 冯德军 
反辐射武器作战效能评估是反辐射武器研制、引进、装备过程中必要的步骤。随着反辐射武器研制的加速发展,反辐射武器的效能评估已经由单纯的精度指标考核向综合对抗能力转变。与此对应,如何综合评估复杂对抗环境下的反辐射武器作战效能...
关键词：系统评估与可行性分析 反辐射武器 武器作战效能 指标聚合 建模评估 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部