Formalization of the inverse kinematics of three-fingered dexterous hand (Q6156933)

In this publication the inverse kinematics of a specific three-fingered dexterous hand is solved using the mathematical theorem proofer HOL light. Some basic definitions are followed by the solutions of a few Paden-Kahan subproblems using screw theory. Finally, the inverse kinematics of the index finger and the thumb is solved as an example by using the forward kinematics in matrix form and applying inverse trigonometric functions and the primarily solved subproblems. Within the article the authors show HOL code lines together with theoretical descriptions of the problem and the solutions.