Formalization of Geometric Algebra in HOL Light

Although the theories of geometric algebra (GA) are widely applied in engineering design and analysis, the studies on their formalization have been scarcely conducted. This paper proposes a relatively complete formalization of GA in HOL Light. Both algebraic and geometric parts of the GA theories are formalized successively. For the algebraic part, a uniform abstract product is proposed to facilitate the formalization of the three basic products based on the formal definition of multivectors with three types of metrics. For the geometric part, the formal formulation is provided for the blades and versors and their relations at first. Then, several commonly used specific spaces are formally represented in the theoretical framework of GA. The novelty of the present paper lies in two aspects: (a) the multivector type, (P,Q,R)geomalg, is defined and the definition provides the most important foundation for the formalization of geometric algebra, and (b) a procedure is developed for automatically proving the properties of GA operations. The present work improves the function of HOL Light and makes the GA-based formal analysis and verification more convenient.