package coq-robot

  1. Overview
  2. No Docs
Formal Foundations for Modeling Robot Manipulators

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

  1. R
    Reynald Affeldt, AIST
  2. C
    Cyril Cohen, Inria
  3. L
    Laurent Thery, Inria

Maintainers

  1. R
    Reynald Affeldt <reynald.affeldt@aist.go.jp>

Sources

0.1.tar.gz
sha512=e4cb8e7857ca4d27d746fb10251b4779a1f59dde8094b6b35300900eac79b9556f697ada33514005a9f78d6a67707225a3c8d5be958437277d3f2a221f3c00cc

Description

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.

Tags

keyword:robotics keyword:3D geometry logpath:robot date:2021-05-11

Published: 11 May 2021

Dependencies (7)

  1. coq-mathcomp-real-closed (>= "1.1.2")
  2. coq-mathcomp-analysis (>= "0.3.6")
  3. coq-mathcomp-field (>= "1.12.0" & < "1.13~")
  4. coq-mathcomp-solvable (>= "1.12.0" & < "1.13~")
  5. coq-mathcomp-algebra (>= "1.12.0" & < "1.13~")
  6. coq-mathcomp-fingroup (>= "1.12.0" & < "1.13~")
  7. coq-mathcomp-ssreflect (>= "1.12.0" & < "1.13~")

Dev Dependencies (1)

  1. coq (>= "8.13" & < "8.14~") | (= "dev")

Used by

None

Conflicts

None