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

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

机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出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.