Geometric Reasoning With Geometric Algebra

Geometric (Clifford) algebra was motivated by geometric considerations and provides a comprehensive algebraic formalism for the expression of geometric ideas [11]. Recent research has shown that this formalism may be effectively used in algebraic approaches for automated geometric reasoning [ 7 , 12 , 14 , 20 , 24 ]. Starting with an introduction to Clifford algebra for n-dimensional Euclidean geometry, this chapter is mainly concerned with the automatic proving of theorems in geometry and identities in Clifford algebra. We explain how to express geometric concepts and relations and how to formulate geometric problems in the language of Clifford algebra. Several examples are given to illustrate a simple mechanism for deriving Clifford algebraic representations of constructed points, or other geometric objects, and how the representations may be used for proving theorems automatically. With explicit representations of geometric objects and simple substitutions, proving a theorem is reduced finally to verifying whether a Clifford algebraic expression is equal to 0. The latter is accomplished in our case by the techniques of term-rewriting for any fixed n.