Formalization and Analysis of Jacobian Matrix in Screw Theory and its Application in Kinematic Singularity

Accurate specification and rigorous analysis of Jacobian matrix are indispensable to guarantee correct evaluation on the manipulator kinematics performance. In this paper, a formal analysis method of the Jacobian matrix in the screw theory is presented by using the higher-order logic theorem prover HOL4. Formalizations of twists and the forward kinematics are characterized with the product of exponential formula and the theory of functional matrices. To the best of our knowledge, this work is the first to formally reason about the spatial Jacobian using theorem proving. The formal modeling and analysis of a 3-DOF planar manipulator substantiate the effectiveness and applicability of the proposed approach to formally verify the kinematics properties of manipulator