Formal analysis of the kinematic Jacobian in screw theory

DOI10.1007/s00165-018-0468-0zbMath1426.70008OpenAlexW2892755039WikidataQ129247445 ScholiaQ129247445MaRDI QIDQ1624599

Aixuan Wu, Yong Guan, Xiumei Yang, Xiaoyu Song, Zhiping Shi, Yong-Dong Li

Publication date: 16 November 2018

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-018-0468-0

zbMATH Keywords

theorem provingforward kinematicsformal methodHOL4Jacobian analysis

Mathematics Subject Classification ID

Kinematics of mechanisms and robots (70B15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Formalization of Euler-Lagrange equation set based on variational calculus in HOL light, Verified interactive computation of definite integrals

Uses Software

• ML
• Isabelle/HOL
• HOL
• Echelon Form

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Generalized Jacobian analysis of lower mobility manipulators
• Formal kinematic analysis of a general 6R manipulator using the screw theory
• Formalization of function matrix theory in HOL
• Formalization of linear space theory in the higher-order logic proving system
• A Uniform Bound for the Jacobian of the Gravitational Force Vector for a Class of Robot Manipulators
• Inverse Velocity and Singularity Analysis of Low-DOF Serial Manipulators
• Theorem Proving in Higher Order Logics