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

来源：软件学报杂志2016年第3期北京时间：

作者：马莎,施智平,李黎明,关永,张杰,Xiaoyu SONG

单位：马莎，轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048;首都师范大学成像技术北京市高精尖创新中心, 北京 10004811,施智平，轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048;北京数学与信息交叉科学2011协同创新中心, 北京 10004802,李黎明，轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004803,关永，轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048;北京数学与信息交叉科学2011协同创新中心, 北京 10004804,张杰，北京化工大学信息科学与技术学院, 北京 10002905,Xiaoyu SONG，Electrical and Computer Engineering, Portland State University, Portland, USA06

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

关键词：几何代数;形式化验证;定理证明;HOL-Light;几何积

基金资助：国家自然科学基金(61170304,61104035,61373034,61303014,61472468,61572331);国际科技合作计划(2010DFB 10930,2011DFG13000);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划(IDHT20150507)