package coq-robot

This library is a formalization of the mathematics of rigid body transformations in the Coq proof-assistant. It can be used to address the forward kinematics problem of robot manipulators. It contains theories for angles, three-dimensional geometry (including three-dimensional rotations, skew-symmetric matrices, quaternions), rigid body transformations (isometries, homogeneous representation, Denavit-Hartenberg convention, screw motions), and an application to the SCARA robot manipulator.