Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

Formal Foundations for Modeling Robot Manipulators

Docker CI

This repository contains an experimental library for the mathematics of rigid body transformations using the Coq proof-assistant and the Mathematical Components library.

Meta

Building and installation instructions

The easiest way to install the latest released version of Formal Foundations for Modeling Robot Manipulators is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-robot

To instead build and install manually, do:

git clone https://github.com/affeldt-aist/robot.git
cd robot
make   # or make -j <number-of-cores-on-your-machine> 
make install

Acknowledgments

Contribution by Damien Rouhling (9b7badc25bf6492f6b84611c7f9d32594b345308)

Grant-in-Aid for Scientific Research Number 15H02687

Disclaimer

This library is still at an experimental stage. Contents may change and definitions and theorems may be renamed. Use at your own risk.

Documentation

This library 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.

Each file is documented more precisely in its header.

Some references used in this work:

Original License

Before [2021-04-29], coq-robot was distributed under the terms of the LGPL-3.0 license.