Automated Geometric Theorem Proving, Clifford Bracket Algebra and Clifford Expansions

  • Hongbo Li
Part of the Trends in Mathematics book series (TM)


We report some of our recent progress on using Clifford bracket algebra to simplify automated geometric theorem-proving via the homogeneous model, and on systematic expansions of Clifford expressions with the purpose of finding the shortest expansions. With such simplification and expansion techniques, we are able to finish some pure geometric computation tasks that are too difficult for other algebraic methods to finish even with the aid of a good PC, and we get better results through a readable procedure.


Automated theorem-proving Clifford algebra bracket algebra invariant theory geometric computation. 

Mathematics Subject Classification (2000)

51K05 14L24 15A66 15A72 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    R. Ablamowicz. CLIFFORD, Maple package
  2. [2]
    M. Barnabei, A. Brini, G.-C. Rota. On the Exterior Calculus of Invariant Theory. J. Algebra 96: 120–160, 1985.MathSciNetCrossRefzbMATHGoogle Scholar
  3. [3]
    P. Bravi and A. Brini. Remarks on Invariant Geometric Calculus, Cayley-Grassmann Algebras and Geometric Clifford Algebras. Manuscript.Google Scholar
  4. [4]
    E. Caianiello. Combinatorics and Renormalization in Quantum Field Theory. Benjamin, Reading, MA, 1973.Google Scholar
  5. [5]
    S. C. Chou, X. S. Gao and J. Z. Zhang. Machine Proofs in Geometry. World Scientific, Singapore, 1994.zbMATHGoogle Scholar
  6. [6]
    H. Crapo and J. Richter-Gebert. Automatic Proving of Geometric Theorems. In: Invariant Methods in Discrete and Computational Geometry, N. White (ed.), pp. 107–139, Kluwer Academic Publishers, 1994.Google Scholar
  7. [7]
    B. Fauser. A Treatise on Quantum Clifford Algebra, Univ. of Konstanz, Germany, 2002. Available at Scholar
  8. [8]
    D. Hestenes and G. Sobczyk. Clifford Algebra to Geometric Calculus,Kluwer, Dordrecht, 1984.CrossRefzbMATHGoogle Scholar
  9. [9]
    B. Kutzler and S. Stifter. On the Application of Buchberger’s Algorithm to Automated Geometry Theorem Proving. J. Symbolic Computation 2: 389–398, 1986.MathSciNetCrossRefzbMATHGoogle Scholar
  10. [10]
    H. Li. New Explorations in Automated Theorem Proving in Geometries, Ph. D. dissertation, Peking Univ., Beijing, 1994.Google Scholar
  11. [11]
    H. Li, D. Hestenes and A. Rockwood. Generalized Homogeneous Coordinates for Computational Geometry. In Geometric Computing with Clifford Algebras, G. Sommer (ed.), pp. 27–60, Springer, Heidelberg, 2001.Google Scholar
  12. [12]
    H. Li. Automated Theorem Proving in the Homogeneous Model with Clifford Bracket Algebra. In: Applications of Geometric Algebra in Computer Science and Engineering, L. Dorst et al. (eds), pp. 69–78, Birkhauser Boston, 2002.CrossRefGoogle Scholar
  13. [13]
    H. Li. Clifford Expansions and Summations. MM Research Report 21, 2002. Available at Scholar
  14. [14]
    B. Sturmfels and N. White. Gröbner Bases and Invariant Theory. Adv. Math. 76: 245–259,1989.MathSciNetCrossRefzbMATHGoogle Scholar
  15. [15]
    B. Sturmfels and W. Whiteley. On the Synthetic Factorization of Homogeneous Invariants. J. Symbolic Computation 11: 439–454, 1991.MathSciNetCrossRefzbMATHGoogle Scholar
  16. [16]
    D. Wang. Geometric reasoning with geometric algebra. In: Geometric Algebra with Applications in Science and Engineering, E. Bayro-Corrochano et al (eds), pp. 89–109, Birkhauser, Boston, 2001.CrossRefGoogle Scholar
  17. [17]
    N. White. The Bracket Ring of Combinatorial Geometry I. Trans. Amer. Math. Soc 202: 79–103, 1975.MathSciNetCrossRefzbMATHGoogle Scholar
  18. [18]
    W. T. Wu. Basic Principles of Mechanical Theorem Proving in Geometries,Volume I: Part of Elementary Geometries. Science Press, Beijing 1984; Springer 1994.Google Scholar
  19. [19]
    I. Yaglom. Felix Klein and Sophus Lie, Birkhauser, Boston, Basel, 1988.zbMATHGoogle Scholar

Copyright information

© Springer Basel AG 2004

Authors and Affiliations

  • Hongbo Li
    • 1
  1. 1.Academy of Mathematics and System SciencesChinese Academy of SciencesBeijingChina

Personalised recommendations