Formal analysis of the kinematic Jacobian in screw theory

DOI10.1007/S00165-018-0468-0MaRDI QIDQ1624599zbMATH OpenOpenAlexWikidataFDO

Authors Zhiping Shi, Aixuan Wu, Xiumei Yang, Yong Guan, Xiaoyu Song, 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

formal methodforward kinematicsHOL4Jacobian analysistheorem proving

Mathematics Subject Classification ID

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

Recommendations

• Formal kinematic analysis of a general 6R manipulator using the screw theory
• Formalization of the inverse kinematics of three-fingered dexterous hand
• Generalized Jacobian analysis of lower mobility manipulators
• Computational kinematics for robotic manipulators: Jacobian problems
• Analytical derivation and application of the Jacobian matrix of parallel kinematic manipulators

Cites work

• A Uniform Bound for the Jacobian of the Gravitational Force Vector for a Class of Robot Manipulators
• Formal kinematic analysis of a general 6R manipulator using the screw theory
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Formalization of function matrix theory in HOL
• Formalization of linear space theory in the higher-order logic proving system
• Generalized Jacobian analysis of lower mobility manipulators
• scientific article; zbMATH DE number 821258 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Inverse Velocity and Singularity Analysis of Low-DOF Serial Manipulators
• Theorem Proving in Higher Order Logics

Cited in

(6)

• Formal kinematic analysis of a general 6R manipulator using the screw theory
• Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
• Verified interactive computation of definite integrals
• scientific article; zbMATH DE number 1304572 (Why is no real title available?)
• A framework for formal verification of robot kinematics
• Formalization of camera pose estimation algorithm based on Rodrigues formula

Describes a project that uses

Uses Software

• Isabelle/HOL
• ML
• HOL
• Echelon Form

This page was built for publication: Formal analysis of the kinematic Jacobian in screw theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1624599)