-
题名函数矩阵及其微积分的高阶逻辑形式化
被引量：2
- 1
-
-
作者
杨秀梅
关永
施智平
吴爱轩
张倩颖
张杰
-
机构
首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室
北京化工大学信息科学与技术学院
-
出处
《计算机科学》
CSCD
北大核心
2016年第11期24-29,共6页
-
基金
国际科技合作计划(2011DFG13000)
国家自然科学基金项目(61170304
+4 种基金
61472468
61572331)
北京市科委项目(Z141100002014001)
北京市教委科研基地建设项目(TJSHG201310028014)
北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助
-
文摘
函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。
-
关键词
函数矩阵
微积分性质
形式化验证
高阶逻辑定理证明
-
Keywords
Function matrix
Calculus
Formal verification
Higher-order logic theorem proving
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名串联机器人雅可比矩阵的高阶逻辑形式化
被引量：4
- 2
-
-
作者
杨秀梅
施智平
吴爱轩
关永
叶世伟
张杰
-
机构
轻型工业机器人与安全验证北京市重点实验室
首都师范大学成像技术北京市高精尖创新中心
北京数学与信息交叉科学协同创新中心
中国科学院研究生院信息科学与工程学院
北京化工大学信息科学与技术学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2016年第4期726-731,共6页
-
基金
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助
国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助
+3 种基金
北京市教委科研基地建设项目(TJSHG201310028014)资助
北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助
北京市优秀人才培养资助项目
北京市属高校青年拔尖人才培育计划资助
-
文摘
机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出100%精确和完备的分析与验证.基于高阶逻辑定理证明技术固有的高可靠性和证明完备性,以运动旋量和串联机器人正向运动学指数积公式为数学基础,在高阶逻辑定理证明器HOL4中建立串联机器人正向运动学的形式化模型,对其旋量法描述的速度雅可比矩阵进行严格的形式化分析与验证.最后通过对Stanford机器人的雅可比矩阵的形式化分析,说明本文形式化工作的实用性和正确性.
-
关键词
机器人雅可比矩阵
运动旋量
HOL4
形式化验证
-
Keywords
roboticjacobian matrix
motion screw
HOL4
formal verification
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名西伯利亚花楸组培苗扩繁与生根培养技术
被引量：3
- 3
-
-
作者
高英凯
范皓翊
吴爱轩
刘洋
建德锋
-
机构
吉林农业科技学院
-
出处
《吉林农业（下半月）》
2016年第5期69-69,共1页
-
基金
吉林农业科技学院大学生科技创新项目(2015)
-
文摘
采用5种不同配比的扩繁培养基配方、4种不同配比生根培养基配方,对西伯利亚花楸组培苗进行扩繁以及诱导生根方面研究,结果得出:MS+6-BA 0.5毫克/升+NAA 0.12毫克/升+KT 0.2毫克/升+IBA 0.05毫克/升配方最有利于苗木扩繁;1/2MS+IBA0.5毫克/升配方最有利于苗木生根,生根率达到100%,平均根数达到4.6,且根系粗壮。
-
关键词
培养基配方
西伯利亚花楸
扩繁
生根
-
分类号
S792.25
[农业科学—林木遗传育种]
-
