Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm

• DOI: 10.1007/s00006-016-0650-5
• Publication Date: 2016-03-22T08:29:13Z
• Authors: Sha Ma; Zhiping Shi; Zhenzhou Shao; Yong Guan; Liming Li; Yongdong Li
• Keywords: Conformal geometric algebra; Geometric Modeling

Conformal geometric algebra (CGA) is an advanced geometric language used in solving three-dimensional Euclidean geometric problems due to its simple, compact and coordinate-free formulations. It promises to stimulate new methods and algorithms in all areas of science dealing with geometric properties, especially for engineering applications. This paper presents a higher-order logic formalization of CGA theories in the HOL-Light theorem prover. First, we formally define the classical algebraic operations and representations of geometric entities in the new framework. Second, we use these results to reason about the correctness of operation properties and geometric features such as the distance between the geometric entities and their rigid transformations in higher-order logic. Finally, in order to demonstrate the practical effectiveness and utilization of this formalization, we use it to formally model the grasping algorithm of a robot based on the conformal geometric control technique and verify the property that whether the robot can grasp firmly or not.