Clifford Algebra, Geometric Computing and Reasoning

Clifford algebra is an algebraic system deeply rooted in geometry. It was named Geometric Algebra by its discoverer W. K. Clifford. In history, many famous mathematicians, E. Cartan, R. Brauer, H. Weyl, C. Chevalley, to name a few, had contributed to its development. In recent years, Clifford algebra has made spectacular achievements in differential geometry, theoretical physics and classical analysis. It is a central tool in modern mathematics and physics, and has wide-ranged applications in robotics, signal processing, computer vision, computational biology, quantum computing, and other high technology fields. In this paper we introduce some applications of Clifford algebra in geometric computing and automated geometric theorem proving. As a very elegant algebraic language for describing and computing geometric problems, Clifford algebra has a variety of coordinate-free and computing-favorable representations for geometric entities, relations and transformations. Therefore, applying Clifford algebra in automated theorem proving can not only make the proof procedures often extremely simple, but also solve open mathematical problems. Nowadays in the world, automated theorem proving has become an important field for applying Clifford algebra.