Clifford Algebra and Automated Geometric Theorem Proving

Clifford algebra is algebraic system deeply rooted in geometry. 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, computer vision, and other enginering fields. In this paper we introduce some applications of Clifford algebra in automated geometric theorem proving the kernel of mathematics mechanization. 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 entites, relations and transformations. Therefore, applying Clifford algebra in automated geometric deduction can not only make the proof procedures extremely simple, but also solve some famous but open mathematical problems. Nowadays in the world, automated geometric deduction has become an important field for applying Clifford algebra.