串联机器人雅可比矩阵的高阶逻辑形式化  

High-order Logic Formalization for Jacobian Matrix of a Serial Robot

作　　者：杨秀梅[1,2] 施智平[1,2] 吴爱轩 关永[1,3] 叶世伟[4] 张杰[5] 

机构地区：[1]轻型工业机器人与安全验证北京市重点实验室,首都师范大学信息工程学院,北京100048 [2]首都师范大学成像技术北京市高精尖创新中心,北京100048 [3]北京数学与信息交叉科学协同创新中心,北京100048 [4]中国科学院研究生院信息科学与工程学院,北京100049 [5]北京化工大学信息科学与技术学院,北京100029

出　　处：《小型微型计算机系统》2016年第4期726-731,共6页Journal of Chinese Computer Systems

基　　金：国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助;北京市优秀人才培养资助项目;北京市属高校青年拔尖人才培育计划资助

摘　　要：机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出100%精确和完备的分析与验证.基于高阶逻辑定理证明技术固有的高可靠性和证明完备性,以运动旋量和串联机器人正向运动学指数积公式为数学基础,在高阶逻辑定理证明器HOL4中建立串联机器人正向运动学的形式化模型,对其旋量法描述的速度雅可比矩阵进行严格的形式化分析与验证.最后通过对Stanford机器人的雅可比矩阵的形式化分析,说明本文形式化工作的实用性和正确性.Jacobian matrix is the important parameter for describingrobotic motion performance,so thatit is very important toguarantee the correctness and reliability of description,analysis and solution of the roboticjacobian matrix.However,the traditional numerical calculation and computer algebra method cannot provide 100% accurate and complete analysis and verification.Consideringthe inherent high reliability and completeness of high-order logic theorem proving technology,this paperfirstly builds theformalization model of serial robots＇ forward kinematics in higher-order logic theorem prover HOL4 based on themathematical foundation of motion screwand product of exponential formula,then formally analyzesand verifies strictly the velocity jacobian matrix of a serial robot described byscrewmethod.Finally,this paper illustrates the availability and correctness of formalization work in this paperby means of formallyanalyzing thejacobian matrix of the Stanford robot.

关 键 词：机器人雅可比矩阵 运动旋量 HOL4 形式化验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]