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

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

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

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


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



本文編號(hào)：3507010