共形几何代数与机器人运动学的形式化

Formalization of Conformal Geometric Algebra and Robot Kinematics

共形几何代数作为一种新的几何表示和计算系统,它为经典几何提供了简洁、直观和统一的齐性代数框架,目前在现代科技的各个领域有很广泛的应用,但是利用共形几何代数进行计算和建模分析的传统方法如数值计算方法和符号方法存在计算不精确等问题.定理证明方法是一种验证系统正确性的严密的形式化方法.在高阶逻辑证明工具HOL-Light中建立共形几何代数系统的形式化模型,提出基本代数运算、几何体表示和几何变换等理论的相关逻辑定义和性质证明.最后为了说明共形几何代数形式化的有效性和实用性,基于共形几何逻辑模型对5R串联机器人的运动学反解进行形式化建模并提出验证方案.

Conformal Geometric Algebra（ CGA） is a modern mathematical language for geometric representation and computation,which provides a unified compact homogeneous algebraic framework for classical geometries. In the last fewyears it has？ been widely ？ used in many high-tech？ fields. Traditionally,CGA based analysis has been done using computer based numerical techniques or symbolic methods. However,both of these techniques cannot guarantee accurate analysis. Theorem proving is one of the rigorous formal methods. This paper established a formal model of CGA in the higher-order-logic proof tool HOL-Light. The correctness of some definitions and properties are proved,mainly including the basic algebraic？ operation,representation of geometric entities and their transformations. In order to illustrate the practical effectiveness and utilization of our work,we use it to formally model the inverse kinematics of 5 degrees of freedom（ DOF） robotic manipulator and propose the corresponding verification scheme.