Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm

DOI10.1007/s00006-016-0650-5zbMath1367.65032OpenAlexW2305158040WikidataQ112879298 ScholiaQ112879298MaRDI QIDQ2360828

Yong-Dong Li, Zhiping Shi, Liming Li, Yong Guan, Sha Ma, Zhen-Zhou Shao

Publication date: 29 June 2017

Published in: Advances in Applied Clifford Algebras (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00006-016-0650-5

zbMATH Keywords

algorithmconformal geometric algebrarobotformalizationHOL-lightgrasping algorithm

Mathematics Subject Classification ID

Numerical aspects of computer graphics, image analysis, and computational geometry (65D18) Robot dynamics and control of rigid bodies (70E60) Clifford algebras, spinors (15A66)

Related Items (6)

Kinematic optimal design of a 2-DoF parallel positioning mechanism employing geometric algebra ⋮ Finite motion analysis of parallel mechanisms with parasitic motions based on conformal geometric algebra ⋮ Formalizing basic quaternionic analysis ⋮ Formalization of functional variation in HOL Light ⋮ Formalization of Euler-Lagrange equation set based on variational calculus in HOL light ⋮ Formalization of geometric algebra in HOL Light

Uses Software

• CLUCalc
• Gaalop
• Nitpick
• HOL Light
• FABRIK
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive 3D space group visualization with CLUCalc and the Clifford geometric algebra description of space groups.
• Inverse kinematics computation in computer graphics and robotics using conformal geometric algebra
• Basic principles of mechanical theorem proving in elementary geometries
• The HOL Light theory of Euclidean space
• Calculation of elements of spin groups using generalized Pauli's theorem
• On the formalization of gamma function in HOL
• ConformalALU: A Conformal Geometric Algebra Coprocessor for Medical Image Processing
• Gaalop—High Performance Parallel Computing Based on Conformal Geometric Algebra
• Towards Self-verification of HOL Light
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm