论文部分内容阅读
机器人雅可比矩阵是描述机器人运动性能的重要参数,保证机器人雅可比矩阵的描述、求解及分析的正确性和可靠性非常重要.然而传统的数值计算与计算机代数符号方法不能给出100%精确和完备的分析与验证.基于高阶逻辑定理证明技术固有的高可靠性和证明完备性,以运动旋量和串联机器人正向运动学指数积公式为数学基础,在高阶逻辑定理证明器HOL4中建立串联机器人正向运动学的形式化模型,对其旋量法描述的速度雅可比矩阵进行严格的形式化分析与验证.最后通过对Stanford机器人的雅可比矩阵的形式化分析,说明本文形式化工作的实用性和正确性.
The Jacobian matrix of robots is an important parameter to describe the robot’s motion performance. It is very important to ensure the correctness and reliability of the description, solution and analysis of robotic Jacobian matrix. However, the traditional numerical and computer algebraic symbol methods can not give 100% Complete analysis and verification.Based on the inherent high reliability and proof completeness of the high-order logic theorem proving technology, based on the mathematical formulas of the motion spin and the positive kinematic exponent product formula of series robot, in the high-order logic theorem prover HOL4 A formalized model of forward kinematics of tandem robot is established and the rigorously formalized analysis and verification of the Jacobian matrix of velocity described by its spin method is carried out.Finally, formal analysis of the Jacobian matrix of Stanford robot shows that this paper formalizes Practicality and correctness of the work.