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

摘要：

机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出100％精确和完备的分析与验证.基于高阶逻辑定理证明技术固有的高可靠性和证明完备性,以运动旋量和串联机器人正向运动学指数积公式为数学基础,在高阶逻辑定理证明器HOI4中建立串联机器人正向运动学的形式化模型,对其旋量法描述的速度雅可比矩阵进行严格的形式化分析与验证.最后通过对Stanford机器人的雅可比矩阵的形式化分析,说明本文形式化工作的实用性和正确性.

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

所属期刊栏目：37

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2016-10-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：726-731