摄动开普勒问题形式化建模与验证

作者：王国辉; 许京然; 刘永梅; 施智平^*; 关永

来源：小型微型计算机系统, 2020, 41(02): 440-444.

• 形式化验证
• 定理证明
• 几何代数
• 摄动
• 卫星轨道

摄动开普勒问题广泛应用于卫星轨道摄动分析,然而卫星轨道摄动分析数学模型的错误将导致灾难性后果.传统的建模与分析方法涉及到矢量代数、旋量代数、复数、四元数等多种不同的代数系统,在各个代数系统相互转换过程中极易引入错误.几何代数方法将多种代数系统统一到相同代数结构中,弥补了传统分析方法的不足.但是基于几何代数的摄动开普勒问题数学模型的正确性并没有通过严格的形式化验证.本文采用高阶逻辑来描述该问题的属性和规范,以公认的逻辑公理和推理规则为基础构建其形式化模型并进行验证,从而最大程度确保数学模型的正确性和分析方法的可靠性.

• 单位
  首都师范大学; 北京城市学院