几何代数的高阶逻辑形式化

几何代数是一种用于描述和计算几何问题的代数语言.由于它统一的表达分析和不依赖于坐标的几何计算等优点现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具, 然而利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.本文在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型,主要包括片积、多重矢量、外积、内积、几何积、几何逆、对偶、基矢量运算和变换算子等的形式化定义和相关性质定理的证明.最后为了说明几何代数形式化的有效性和实用性,本文在共形几何代数空间中对刚体运动问题提供了一种新的简单有效的形式化建模与验证方法.

Formalization of Geometric Algebra Theories in Higher-Order Logic

Geometric algebra (GA) is an algebraic language used to describe and calculate geometric problems. Because of its unified expression and geometric calculation with coordinate-free has now become an important theoretical foundation and calculation tool in mathematical analysis, theoretical physics, geometry and other fields. It has been widely used in the areas of modern science and technology. Traditionally, GA based analysis has been done using computer based numerical techniques or symbolic methods. However, both of these techniques cannot guarantee accurate analysis for safety-critical areas. The higher order-logic theorem proving is one of the rigorous formal methods. This paper established a formal model of GA in the higher-order logic proof tool HOL-Light. The correctness of some definitions and properties are proved, mainly including blade, multivector, outer product, inner product, geometric product, inverse, dual, operation rules of basis vector and transform operator. In order to illustrate the practical effectiveness and utilization of this formalization, we use it to establish conformal geometric model, which can provide a simple and effective way on rigid body motion verification.