文献类型：期刊文章

作　　者：杨秀梅[1] 关永[1] 施智平[1] 吴爱轩[1] 张倩颖[1] 张杰[2]

机构地区：[1]首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室,北京100048 [2]北京化工大学信息科学与技术学院,北京100029

出　　处：《计算机科学》

基　　金：国际科技合作计划(2011DFG13000);国家自然科学基金项目(61170304;61472468;61572331);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助

年　　份：2016

卷　　号：43

期　　号：11

起止页码：24-29

语　　种：中文

收录情况：BDHX、BDHX2014、CSA、CSCD、CSCD_E2015_2016、IC、JST、RCCSE、UPD、ZGKJHX、核心刊

摘　　要：函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。

关 键 词：函数矩阵 微积分性质  形式化验证 高阶逻辑定理证明  

分 类 号：TP301]