%0 Journal Article
%T 串联机器人雅可比矩阵的高阶逻辑形式化
%A 关永
%A 叶世伟
%A 吴爱轩
%A 张杰
%A 施智平
%A 杨秀梅
%J 中山大学学报（自然科学版）
%D 2016
%X 摘要 机器人雅可比矩阵是描述机器人运动性能的重要参数，保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出100%精确和完备的分析与验证.基于高阶逻辑定理证明技术固有的高可靠性和证明完备性，以运动旋量和串联机器人正向运动学指数积公式为数学基础，在高阶逻辑定理证明器HOL4中建立串联机器人正向运动学的形式化模型，对其旋量法描述的速度雅可比矩阵进行严格的形式化分析与验证.最后通过对Stanford机器人的雅可比矩阵的形式化分析，说明本文形式化工作的实用性和正确性
%K 机器人雅可比矩阵
%K 运动旋量
%K HOL4
%K 形式化验证
%U http://xwxt.sict.ac.cn/CN/abstract/abstract3348.shtml