基于幾何代數(shù)的高階邏輯形式化建模

　　幾何代數(shù)是一種用于描述和計(jì)算幾何問(wèn)題的代數(shù)語(yǔ)言，由于它統(tǒng)一表達(dá)分析和不依賴于坐標(biāo)的幾何計(jì)算等優(yōu)點(diǎn)，現(xiàn)已成為數(shù)學(xué)分析、理論物理、幾何學(xué)、工程應(yīng)用等領(lǐng)域重要的理論基礎(chǔ)和計(jì)算工具．然而，利用幾何代數(shù)進(jìn)行計(jì)算和建模分析的傳統(tǒng)方法，如數(shù)值計(jì)算方法和符號(hào)方法等，都存在計(jì)算不精確或者不完備等問(wèn)題，高階邏輯定理證明是驗(yàn)證系統(tǒng)正確的一種嚴(yán)密的形式化方法．在高階邏輯證明工具HOL-Light中建立了幾何代數(shù)系統(tǒng)的形式化模型，主要包括片積、多重矢量、外積、內(nèi)積、幾何積、幾何逆、對(duì)偶、基矢量運(yùn)算和變換算子等的形式化定義和相關(guān)性質(zhì)定理的證明．最后，為了說(shuō)明幾何代數(shù)形式化的有效性和實(shí)用性，在共形幾何代數(shù)空間中，給剛體運(yùn)動(dòng)問(wèn)題提供了一種簡(jiǎn)單有效的形式化建模與驗(yàn)證方法．