Abstract:
Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral
step of their design. The main idea behind kinematic analysis is to study the motion of the
robot based on the geometrical relationship of the robotic links and their joints. Given the
continuous nature of kinematic analysis, traditional computer-based verification methods,
such as simulation, numerical methods or model checking, fail to provide reliable results.
This fact makes robotic designs erroneous, which may lead to catastrophic consequences
given the safety-perilous sort of robotic applications. Leveraging upon the high expres siveness of higher-order logic, we used higher-order-logic theorem proving for conducting
formal kinematic analysis. As a first step towards this direction, we utilize the geometry
theory of HOL-Light to develop formal reasoning support for the kinematic analysis of
a two-link planar manipulator, which forms the basis for many mechanical structures in
robotics. To prove the usefulness of our foundational formalization, we put forward the
formal kinematic analysis of a biped walking robot.
