攝動開普勒問題形式化建模與驗證
發(fā)布時間:2021-11-20 09:08
攝動開普勒問題廣泛應(yīng)用于衛(wèi)星軌道攝動分析,然而衛(wèi)星軌道攝動分析數(shù)學模型的錯誤將導致災(zāi)難性后果.傳統(tǒng)的建模與分析方法涉及到矢量代數(shù)、旋量代數(shù)、復數(shù)、四元數(shù)等多種不同的代數(shù)系統(tǒng),在各個代數(shù)系統(tǒng)相互轉(zhuǎn)換過程中極易引入錯誤.幾何代數(shù)方法將多種代數(shù)系統(tǒng)統(tǒng)一到相同代數(shù)結(jié)構(gòu)中,彌補了傳統(tǒng)分析方法的不足.但是基于幾何代數(shù)的攝動開普勒問題數(shù)學模型的正確性并沒有通過嚴格的形式化驗證.本文采用高階邏輯來描述該問題的屬性和規(guī)范,以公認的邏輯公理和推理規(guī)則為基礎(chǔ)構(gòu)建其形式化模型并進行驗證,從而最大程度確保數(shù)學模型的正確性和分析方法的可靠性.
【文章來源】:小型微型計算機系統(tǒng). 2020,41(02)北大核心CSCD
【文章頁數(shù)】:5 頁
【文章目錄】:
1 引言
2 幾何代數(shù)基礎(chǔ)及其形式化
2.1 幾何代數(shù)基本運算及其性質(zhì)的形式化
2.2 位置矢量與旋量
2.3 多重向量微分形式化
3 衛(wèi)星攝動開普勒問題形式化建模
3.1 慣性坐標系中攝動開普勒方程形式化
3.2 基于幾何代數(shù)的攝動開普勒方程形式化
4 衛(wèi)星攝動開普勒問題形式化驗證
4.1 地球與衛(wèi)星相對位置矢量形式化定義
4.2 地球與衛(wèi)星相對位置形式化相關(guān)定理
4.3 基于幾何代數(shù)攝動開普勒方程形式化推導
4.4 攝動開普勒問題幾何代數(shù)模型與慣性坐標模型等價性證明
5 結(jié)論
【參考文獻】:
期刊論文
[1]幾何代數(shù)的高階邏輯形式化[J]. 馬莎,施智平,李黎明,關(guān)永,張杰,Xiaoyu SONG. 軟件學報. 2016(03)
[2]幾何代數(shù)及其在攝動Kepler問題中的應(yīng)用[J]. 方茹,曹喜濱,張錦繡. 哈爾濱工業(yè)大學學報. 2008(02)
本文編號:3507010
【文章來源】:小型微型計算機系統(tǒng). 2020,41(02)北大核心CSCD
【文章頁數(shù)】:5 頁
【文章目錄】:
1 引言
2 幾何代數(shù)基礎(chǔ)及其形式化
2.1 幾何代數(shù)基本運算及其性質(zhì)的形式化
2.2 位置矢量與旋量
2.3 多重向量微分形式化
3 衛(wèi)星攝動開普勒問題形式化建模
3.1 慣性坐標系中攝動開普勒方程形式化
3.2 基于幾何代數(shù)的攝動開普勒方程形式化
4 衛(wèi)星攝動開普勒問題形式化驗證
4.1 地球與衛(wèi)星相對位置矢量形式化定義
4.2 地球與衛(wèi)星相對位置形式化相關(guān)定理
4.3 基于幾何代數(shù)攝動開普勒方程形式化推導
4.4 攝動開普勒問題幾何代數(shù)模型與慣性坐標模型等價性證明
5 結(jié)論
【參考文獻】:
期刊論文
[1]幾何代數(shù)的高階邏輯形式化[J]. 馬莎,施智平,李黎明,關(guān)永,張杰,Xiaoyu SONG. 軟件學報. 2016(03)
[2]幾何代數(shù)及其在攝動Kepler問題中的應(yīng)用[J]. 方茹,曹喜濱,張錦繡. 哈爾濱工業(yè)大學學報. 2008(02)
本文編號:3507010
本文鏈接:http://sikaile.net/kejilunwen/hangkongsky/3507010.html
最近更新
教材專著