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

Xiaoyu SONG1关永2张杰3施智平2李黎明2马莎2

1.首都师范大学; 2.北京化工大学; 3.波特兰州立大学;

摘要：

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

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

所属期刊栏目：27

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金61170304,61104035,61373034,61303014,61472468,61572331;国际科技合作计划2010DFB10930,2011DFG13000;北京市科委项目Z141100002014001;北京市教委科研基地建设项目TJSHG201310028014;北京市属高等学校创新团队建设与教师职业发展计划IDHT20150507National Natural Science Foundation of China61170304,61104035,61373034,61303014,61472468,61572331;Int'l Cooperation Program on Science and Technology2010DFB10930,2011DFG13000;Beijing Municipal Science and technology projectZ141100002014001;Scientific Research Base Development Program of the Beijing Municipal Commission of EducationTJSHG201310028014;Project of Construction of Innovative Teams and Teacher Career Development for Universities and Colleges under Beijing MunicipalityIDHT20150507

在线出版日期：2016-08-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共22页

页码：495-516