Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm
Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm
复制标题
共形几何代数的高阶逻辑形式化及其在机器人操纵算法验证中的应用
DOI：
10.1007/s00006-016-0650-5
复制
发表时间：
2016
影响因子：
1.5
通讯作者：
Li Yongdong
中科院分区：
文献类型：
--
作者：
Ma Sha;Shi Zhiping;Shao Zhenzhou;Guan Yong;Li Liming;Li Yongdong
共形几何代数（Conformal geometric algebra，CGA）是一种用于求解三维欧几里德几何问题的高级几何语言，它具有简单、紧凑和无坐标的特点。它有望在处理几何性质的所有科学领域，特别是在工程应用中，激发新的方法和算法。本文提出了一种高阶逻辑形式化的CGA理论的HOL-Light定理证明。首先，我们正式定义了经典的代数运算和几何实体的表示在新的框架。其次，我们使用这些结果的正确性的操作属性和几何特征，如几何实体之间的距离和它们的刚性变换在高阶逻辑的原因。最后，为了证明该形式化方法的实用性和有效性，我们利用该形式化方法对基于共形几何控制技术的机器人抓取算法进行了形式化建模，并验证了该机器人是否能够牢固抓取。
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.