Skip to main content
SpringerLink
Log in

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

  • Published:
Advances in Applied Clifford Algebras Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Aristidou A., Lasenby J.: FABRIK: a fast, iterative solver for the inverse kinematics problem. Graph. Models 73(4), 243–260 (2011)

    Article  Google Scholar 

  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)

  3. Bayro-Corrochano E., Zamora-Esquivel J.: Differential and inverse kinematics of robot devices using conformal geometric algebra. Robotica 25(1), 43–61 (2007)

    Article  Google Scholar 

  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)

  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)

    Chapter  Google Scholar 

  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)

  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. 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)

    Article  MathSciNet  Google Scholar 

  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)

  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)

    MathSciNet  Google Scholar 

  11. Harrison, J.: HOL Light: A Tutorial Introduction. Lecture Notes in C Computer Science, pp. 265–269 (1996)

  12. Harrison, J.: Towards Self-verification of HOL Light. Lecture Notes in Computer Science, pp. 177–191 (2006)

  13. Harrison, J.: https://code.google.com/p/hol-light/source/browse/trunk/Multivariate/clifford.ml (2010)

  14. Harrison J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50(2), 173–190 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  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)

  16. Hestenes D.: Spacetime physics with geometric algebra. Am. J. Phys. 71(7), 691–714 (2003)

    Article  ADS  Google Scholar 

  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)

  18. Hildenbrand, D.: Geometric computing in Computer Graphics and Robotics using Conformal Geometric Algebra. PhD Thesis, Technische Universitaet Darmstadt (2007)

  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)

    Article  MathSciNet  MATH  Google Scholar 

  20. Hildenbrand D.: Foundations of geometric algebra computing. Geom. Comput. 1479(4), 27–30 (2012)

    Google Scholar 

  21. Hildenbrand, D., Koch, A.: Gaalop: high performance computing based on conformal geometric algebra. Geom. Comput. (2013)

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

  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. 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)

  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)

  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)

  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)

  30. Lounesto P.: Clifford algebras and Hestenes spinors. Found. Phys. 23(9), 1203–1237 (1993)

    Article  ADS  MathSciNet  Google Scholar 

  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)

  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)

  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. Shirokov D.: Calculation of elements of spin groups using generalized Pauli’s theorem. Adv. Appl. Clifford Algebras 25(1), 227–244 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  35. Siddique, U., Hasan, O.: On the formalization of gamma function in HOL. J. Autom. Reason. 407–429 (2014)

  36. Suter, J.: Geometric Algebra Primer. Available: http://www.jaapsuter.com (2003)

  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)

  38. Wu W.J.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221–252 (1986)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. College of Information Engineering, Capital Normal University, Beijing, China

    Sha Ma, Zhiping Shi, Zhenzhou Shao, Yong Guan, Liming Li & Yongdong Li

  2. Beijing Advanced Innovation Center for Imaging Technology, Beijing, China

    Zhiping Shi, Yong Guan & Liming Li

  3. Beijing Key Laboratory of Light Industrial Robot and Safety Verification, Beijing, China

    Zhenzhou Shao & Yongdong Li

Authors
  1. Sha Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhiping Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhenzhou Shao
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yong Guan
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Liming Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Yongdong Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhiping Shi.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ma, S., Shi, Z., Shao, Z. et al. Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm. Adv. Appl. Clifford Algebras 26, 1305–1330 (2016). https://doi.org/10.1007/s00006-016-0650-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00006-016-0650-5

Keywords

Search

Navigation