Advances in Applied Clifford Algebras

, Volume 26, Issue 4, pp 1305–1330 | Cite as

Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm

  • Sha Ma
  • Zhiping Shi
  • Zhenzhou Shao
  • Yong Guan
  • Liming Li
  • Yongdong Li


Conformal geometric algebra (CGA) is an advanced geometric language used in solving three-dimensional Euclidean geometric problems due to its simple, compact and coordinate-free formulations. It promises to stimulate new methods and algorithms in all areas of science dealing with geometric properties, especially for engineering applications. This paper presents a higher-order logic formalization of CGA theories in the HOL-Light theorem prover. First, we formally define the classical algebraic operations and representations of geometric entities in the new framework. Second, we use these results to reason about the correctness of operation properties and geometric features such as the distance between the geometric entities and their rigid transformations in higher-order logic. Finally, in order to demonstrate the practical effectiveness and utilization of this formalization, we use it to formally model the grasping algorithm of a robot based on the conformal geometric control technique and verify the property that whether the robot can grasp firmly or not.


Conformal geometric algebra HOL-light Formalization Grasping algorithm Robot 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aristidou A., Lasenby J.: FABRIK: a fast, iterative solver for the inverse kinematics problem. Graph. Models 73(4), 243–260 (2011)CrossRefGoogle Scholar
  2. 2.
    Bayro-Corrochano, E., Bernal-Marin, M.: Generalized hough transform and conformal geometric algebra to detect lines and planes for building 3D maps and robot navigation. In: Intelligent Robots and Systems (IROS), IEEE/RSJ International Conference on, pp. 810–815 (2010)Google Scholar
  3. 3.
    Bayro-Corrochano E., Zamora-Esquivel J.: Differential and inverse kinematics of robot devices using conformal geometric algebra. Robotica 25(1), 43–61 (2007)CrossRefGoogle Scholar
  4. 4.
    Blanchette, J.C., Nipkow, T.: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. Lecture Notes in Computer Science, pp. 131–146 (2010)Google Scholar
  5. 5.
    Buchholz S., Sommer G.: Introduction to neural computation in Clifford algebra. In: Sommer, G. (ed.) Geometric Computing with Clifford Algebras, pp. 291–314. Springer-Verlag, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Carbajal-Espinosa, O., Osuna-Gonzalez, G., Gonzalez-Jimenez, L. et al.: Visual servoing and robust object manipulation using symmetries and conformai geometric algebra. In: Humanoid Robots (Humanoids), IEEE-RAS International Conference on, pp. 1051–1056 (2014)Google Scholar
  7. 7.
    Dorst L., Fontijne D., Mann S.: Geometric Algebra for Computer Science: An Object Oriented approach to Geometry. Morgan Kaufmann, San Francisco (2007)Google Scholar
  8. 8.
    Franchini S., Gentile A., Sorbello F. et al.: ConformalALU: a conformal geometric algebra coprocessor for medical image processing. IEEE Trans. Comput. 64(4), 955–970 (2015)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Gonzalez-Jimenez, L.E., Carbajal-Espinosa, O.E., Bayro-Corrochano, E.: Geometric techniques for the kinematic modeling and control of robotic manipulators. In: Proc. of IEEE ICRA, pp. 5831–5836 (2011)Google Scholar
  10. 10.
    Han D.S., Yang Q.L., Xing J.C.: UML-Based modeling and formal verification for software self-adaptation. J. Softw. 26(4), 730–746 (2015)MathSciNetGoogle Scholar
  11. 11.
    Harrison, J.: HOL Light: A Tutorial Introduction. Lecture Notes in C Computer Science, pp. 265–269 (1996)Google Scholar
  12. 12.
    Harrison, J.: Towards Self-verification of HOL Light. Lecture Notes in Computer Science, pp. 177–191 (2006)Google Scholar
  13. 13.
  14. 14.
    Harrison J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50(2), 173–190 (2013)MathSciNetCrossRefMATHGoogle Scholar
  15. 15.
    Hasan, O., Ahmad, M.: Formal analysis of steady state errors in feedback control systems using HOL-light. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), 18–22 March, Grenoble, France, pp. 1423–1426 (2013)Google Scholar
  16. 16.
    Hestenes D.: Spacetime physics with geometric algebra. Am. J. Phys. 71(7), 691–714 (2003)ADSCrossRefGoogle Scholar
  17. 17.
    Hildenbrand, D., Bayro-Corrochano, E., Zamora, J.: Advanced geometric approach for graphics and visual guided robot object manipulation. In: Proc. of IEEE ICRA, pp. 4727–4732 (2005)Google Scholar
  18. 18.
    Hildenbrand, D.: Geometric computing in Computer Graphics and Robotics using Conformal Geometric Algebra. PhD Thesis, Technische Universitaet Darmstadt (2007)Google Scholar
  19. 19.
    Hildenbrand D., Zamora J., Bayro-Corrochano E.: Inverse kinematics computation in computer graphics and robotics using conformal geometric algebra. Adv. Appl. Clifford Algebras 18(3), 699–713 (2008)MathSciNetCrossRefMATHGoogle Scholar
  20. 20.
    Hildenbrand D.: Foundations of geometric algebra computing. Geom. Comput. 1479(4), 27–30 (2012)Google Scholar
  21. 21.
    Hildenbrand, D., Koch, A.: Gaalop: high performance computing based on conformal geometric algebra. Geom. Comput. (2013)Google Scholar
  22. 22.
    Hitzer E., Perwass C.: Interactive 3D space group visualization with CLUCalc and the clifford geometric algebra description of space groups. Adv. Appl. Clifford Algebras 20(4), 631–658 (2010)MathSciNetCrossRefMATHGoogle Scholar
  23. 23.
    Kim J.S., Jin H.J., Park J.H.: Inverse kinematics and geometric singularity analysis of a 3-SPS/S redundant motion mechanism using conformal geometric algebra. Mech. Mach. Theory 90, 23–36 (2015)CrossRefGoogle Scholar
  24. 24.
    Klein, G., Elphinstone, K., Heiser, G., et al.: seL4: Formal Verification of an OS Kernel. Acm Symposium on Operating Systems Principles, pp. 207–220 (2009)Google Scholar
  25. 25.
    Li H.: Conformal geometric algebra and algebraic manipulations of geometric invariants. J. Comput. Aided Des. Comput. Graph. 18(7), 902–911 (2006)Google Scholar
  26. 26.
    Li, H.: Automated theorem proving in the homogeneous model with Clifford bracket algebra. In: Dorst, L. (eds.) Applications of Geometric Algebra in Computer Science and Engineering, pp. 69–78. Boston (2002)Google Scholar
  27. 27.
    Li, M., Guan, J.: Possibilistic C-Spherical Shell clustering algorithm based on conformai geometric algebra. Signal Processing (ICSP), IEEE 10th International Conference on, pp. 1347–1350 (2010)Google Scholar
  28. 28.
    Li, H., Hestenes, D., Rockwood, A.: A universal model for conformal geometries of euclidean, spherical and double-hyperbolic spaces. Geom. Comput. Clifford Algebras, 77–104 (2001)Google Scholar
  29. 29.
    Lopez-Franco, C., Arana-Daniel, N., Bayro-Corrochano, E.: Vision-based robot control with omnidirectional cameras and conformal geometric algebra. In: IEEE International Conference on Robotics and Automation (ICRA), pp. 2543–2548 (2010)Google Scholar
  30. 30.
    Lounesto P.: Clifford algebras and Hestenes spinors. Found. Phys. 23(9), 1203–1237 (1993)ADSMathSciNetCrossRefGoogle Scholar
  31. 31.
    Oviedo-Barriga, J., Carbajal-Espinosa, O., Gonzalez-Jimenez, L. et al.: Robust tracking of bio-inspired references for a biped robot using geometric algebra and sliding modes. In: Proc. of IEEE ICRA, pp. 5317–5322 (2013)Google Scholar
  32. 32.
    Pham, M.T., Tachibana, K., Yoshikawa, T. et al.: A clustering method for geometric data based on approximation using conformal geometric algebra. In: IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), pp. 2540–2545 (2011)Google Scholar
  33. 33.
    Resten Y., Maler O., Marcus M. et al.: Symbolic model checking with rich assertional languages. Comput. Aided Verification 43(2), 424–435 (2006)Google Scholar
  34. 34.
    Shirokov D.: Calculation of elements of spin groups using generalized Pauli’s theorem. Adv. Appl. Clifford Algebras 25(1), 227–244 (2014)MathSciNetCrossRefMATHGoogle Scholar
  35. 35.
    Siddique, U., Hasan, O.: On the formalization of gamma function in HOL. J. Autom. Reason. 407–429 (2014)Google Scholar
  36. 36.
    Suter, J.: Geometric Algebra Primer. Available: (2003)
  37. 37.
    Wang, C., Wu, H., Miao, Q.: Inverse kinematics computation in robotics using Conformal Geometric Algebra. Technology and Innovation Conference (ITIC), International pp. 1–5. IET (2009)Google Scholar
  38. 38.
    Wu W.J.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221–252 (1986)CrossRefMATHGoogle Scholar

Copyright information

© Springer International Publishing 2016

Authors and Affiliations

  • Sha Ma
    • 1
  • Zhiping Shi
    • 1
    • 2
  • Zhenzhou Shao
    • 1
    • 3
  • Yong Guan
    • 1
    • 2
  • Liming Li
    • 1
    • 2
  • Yongdong Li
    • 1
    • 3
  1. 1.College of Information EngineeringCapital Normal UniversityBeijingChina
  2. 2.Beijing Advanced Innovation Center for Imaging TechnologyBeijingChina
  3. 3.Beijing Key Laboratory of Light Industrial Robot and Safety VerificationBeijingChina

Personalised recommendations