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

• 作者: Xiaoyu SONG 关永 张杰 施智平 李黎明 马莎
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 几何代数 形式化验证 定理证明 HOL-Light 几何积
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 软件形式化方法与应用专题
• 页码范围: 495-516
• 页数: 22页
• 分类号: TP301
• 字数: 17134字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004977

摘要

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