函数矩阵及其微积分的高阶逻辑形式化

• 作者: 关永 吴爱轩 张倩颖 张杰 施智平 杨秀梅
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 函数矩阵 微积分性质 形式化验证 高阶逻辑定理证明
• 年，卷（期）: 2016,（11）
• 页码范围: 24-29
• 页数: 6页
• 分类号: TP301
• 字数: 7667字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2016.11.005

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰		60	501	11.0	20.0
2	关永	首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室	95	1336	17.0	33.0
3	施智平	首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室	24	145	8.0	11.0
4	张倩颖	首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室	4	19	2.0	4.0
5	杨秀梅	首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室	1	0	0.0	0.0
6	吴爱轩	首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室	1	0	0.0	0.0