攝動開普勒問題廣泛應用于衛(wèi)星軌道攝動分析,然而衛(wèi)星軌道攝動分析數(shù)學模型的錯誤將導致災難性后果.傳統(tǒng)的建模與分析方法涉及到矢量代數(shù)、旋量代數(shù)、復數(shù)、四元數(shù)等多種不同的代數(shù)系統(tǒng),在各個代數(shù)系統(tǒng)相互轉換過程中極易引入錯誤.幾何代數(shù)方法將多種代數(shù)系統(tǒng)統(tǒng)一到相同代數(shù)結構中,彌補了傳統(tǒng)分析方法的不足.但是基于幾何代數(shù)的攝動開普勒問題數(shù)學模型的正確性并沒有通過嚴格的形式化驗證.本文采用高階邏輯來描述該問題的屬性和規(guī)范,以公認的邏輯公理和推理規(guī)則為基礎構建其形式化模型并進行驗證,從而最大程度確保數(shù)學模型的正確性和分析方法的可靠性. 

【文章來源】：小型微型計算機系統(tǒng). 2020,41(02)北大核心CSCD

【文章頁數(shù)】：5 頁

【文章目錄】：
1 引言
2 幾何代數(shù)基礎及其形式化
    2.1 幾何代數(shù)基本運算及其性質的形式化
    2.2 位置矢量與旋量
    2.3 多重向量微分形式化
3 衛(wèi)星攝動開普勒問題形式化建模
    3.1 慣性坐標系中攝動開普勒方程形式化
    3.2 基于幾何代數(shù)的攝動開普勒方程形式化
4 衛(wèi)星攝動開普勒問題形式化驗證
    4.1 地球與衛(wèi)星相對位置矢量形式化定義
    4.2 地球與衛(wèi)星相對位置形式化相關定理
    4.3 基于幾何代數(shù)攝動開普勒方程形式化推導
    4.4 攝動開普勒問題幾何代數(shù)模型與慣性坐標模型等價性證明
5 結論


【參考文獻】：
期刊論文
[1]幾何代數(shù)的高階邏輯形式化[J]. 馬莎,施智平,李黎明,關永,張杰,Xiaoyu SONG.  軟件學報. 2016(03)
[2]幾何代數(shù)及其在攝動Kepler問題中的應用[J]. 方茹,曹喜濱,張錦繡.  哈爾濱工業(yè)大學學報. 2008(02)



本文編號：3507010