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

Formal Modeling and Verification of Perturbed Kepler Problem

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

The perturbation Kepler problem is widely used in satellite orbital perturbation analysis,but some errors in the mathematical model of satellite orbit perturbation analysis will lead to catastrophic consequences. Traditional modeling and analysis methods involve many different algebraic systems,such as vector algebra,spin algebra,complex number,quaternion,etc.,and it is easy to introduce erroin the process of mutual conversion of each algebraic system. The geometric algebra method unifies a variety of algebraic systems into the same algebraic structure,making up for the shortcomings of traditional analytical methods. However,the correctness of the mathematical model of the perturbation Kepler problem based on geometric algebra has not passed the strict formal verification. In this paper,high-order logic is used to describe the attributes and norms of the problem. The formal model is constructed and verified based on the recognized logical axioms and inference rules,so as to ensure the correctness of the mathematical model and the reliability of the analytical method.