单球驱动平衡机器人的运动学和动力学形式化验证方法

本公开实施例公开了一种单球驱动平衡机器人的运动学和动力学形式化验证方法，所述方法包括：建立单球驱动平衡机器人相关的坐标系；建立齐次变换矩阵的高阶逻辑模型；建立矩阵值函数的微分的高阶逻辑模型和空间速度的高阶逻辑模型；建立向量值函数有微分的高阶逻辑模型、向量值函数的微分的高阶逻辑模型、旋转矩阵和位置向量的高阶逻辑模型；建立单球驱动平衡机器人的拉格朗日方程的高阶逻辑模型；形式化描述单球驱动平衡机器人运动学和动力学相关的逻辑命题，运动学相关的逻辑命题包括末端位姿、空间速度、末端速度的逻辑命题；动力学相关的逻辑命题包括拉格朗日动力学方程的逻辑命题；利用高阶逻辑定理证明器证明验证上述逻辑命题是否成立。