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

发布时间：2021-11-20 09:08

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

【文章来源】：小型微型计算机系统. 2020,41(02)北大核心CSCD

【文章页数】：5 页

【文章目录】：
1 引言
2 几何代数基础及其形式化
    2.1 几何代数基本运算及其性质的形式化
    2.2 位置矢量与旋量
    2.3 多重向量微分形式化
3 卫星摄动开普勒问题形式化建模
    3.1 惯性坐标系中摄动开普勒方程形式化
    3.2 基于几何代数的摄动开普勒方程形式化
4 卫星摄动开普勒问题形式化验证
    4.1 地球与卫星相对位置矢量形式化定义
    4.2 地球与卫星相对位置形式化相关定理
    4.3 基于几何代数摄动开普勒方程形式化推导
    4.4 摄动开普勒问题几何代数模型与惯性坐标模型等价性证明
5 结论


【参考文献】：
期刊论文
[1]几何代数的高阶逻辑形式化[J]. 马莎,施智平,李黎明,关永,张杰,Xiaoyu SONG.  软件学报. 2016(03)
[2]几何代数及其在摄动Kepler问题中的应用[J]. 方茹,曹喜滨,张锦绣.  哈尔滨工业大学学报. 2008(02)



本文编号：3507010