摘要
机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出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.
出处
《小型微型计算机系统》
CSCD
北大核心
2016年第4期726-731,共6页
Journal of Chinese Computer Systems
基金
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助
国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助
北京市教委科研基地建设项目(TJSHG201310028014)资助
北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助
北京市优秀人才培养资助项目
北京市属高校青年拔尖人才培育计划资助