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

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