本書(shū)以幾何代數(shù)理論體系與自動(dòng)定理證明思想為指導(dǎo)，系統(tǒng)深入地研究了幾何代數(shù)的形式化理論與公理化體系，構(gòu)建了一個(gè)兼具代數(shù)推理和幾何解算能力的統(tǒng)一形式化數(shù)學(xué)定理體系，對(duì)代數(shù)與幾何從概念上進(jìn)行了融合與拓展、從描述方法和運(yùn)算法則上進(jìn)行了綜合與歸納，為代數(shù)理論賦予了“形”的特征，為幾何理論提供了“數(shù)”的內(nèi)涵，并將其初步應(yīng)用于實(shí)際物理問(wèn)題的證明，內(nèi)容涵蓋了自動(dòng)定理證明、機(jī)器人、形式化驗(yàn)證等人工智能領(lǐng)域。全書(shū)主要內(nèi)容包括：幾何代數(shù)理論的進(jìn)展、形式化理論；HOLLight定理證明器體系；幾何代數(shù)結(jié)構(gòu)的形式化；幾何與物理解釋的形式化；單目相機(jī)姿態(tài)估計(jì)模型的形式化分析、對(duì)稱(chēng)陀螺運(yùn)動(dòng)的形式化分析等初步應(yīng)用案例。作者長(zhǎng)期對(duì)系統(tǒng)形式化與自動(dòng)定理證明進(jìn)行深入研究，并在機(jī)器人安全驗(yàn)證等領(lǐng)域持續(xù)實(shí)踐迭代，本書(shū)是對(duì)該過(guò)程成果的高度凝練與系統(tǒng)總結(jié)。
更多科學(xué)出版社服務(wù)，請(qǐng)掃碼獲取。
目錄
序
前言
第1章 緒論 1
1.1 背景 1
1.2 幾何代數(shù)與數(shù)學(xué)形式化 2
1.2.1 幾何代數(shù)的發(fā)展歷史 2
1.2.2 數(shù)學(xué)理論形式化及其發(fā)展歷史 4
1.3 主要內(nèi)容 11
1.4 本書(shū)結(jié)構(gòu) 13
1.5 符號(hào)約定 14
參考文獻(xiàn) 15
第2章 幾何代數(shù)簡(jiǎn)介 22
2.1 二次型空間 22
2.2 結(jié)構(gòu)、元素、運(yùn)算和子空間 23
2.2.1 公理性質(zhì) 23
2.2.2 幾何代數(shù)基底 24
2.2.3 多重向量 27
2.2.4 內(nèi)積和外積 27
2.3 幾何解釋 29
參考文獻(xiàn) 32
第3章 幾何代數(shù)結(jié)構(gòu)的形式化 33
3.1 元素與運(yùn)算 33
3.1.1 多重向量 34
3.1.2 積運(yùn)算 39
3.1.3 幾何積的逆運(yùn)算 41
3.1.4 運(yùn)算性質(zhì)和自動(dòng)解算程序 42
3.2 Blade 的定義及性質(zhì) 47
3.2.1 定義 47
3.2.2 幾何積 48
3.2.3 外積 49
3.2.4 線性相關(guān) 51
3.2.5 標(biāo)量積 53
3.2.6 反轉(zhuǎn) 53
3.2.7 共軛 54
3.2.8 范數(shù) 55
3.2.9 內(nèi)積 56
3.2.10 對(duì)偶 58
3.2.11 逆和偽逆 60
3.2.12 水平投影 62
3.2.13 垂直投影 63
3.2.14 相交和連接 63
3.3 Versor 的定義及性質(zhì) 64
3.3.1 定義 64
3.3.2 性質(zhì) 67
3.3.3 幾何變換 68
3.4 多重向量的微分 68
3.5 具體代數(shù)實(shí)例 69
3.5.1 Gibbs 向量代數(shù) 69
3.5.2 復(fù)數(shù) 70
3.5.3 四元數(shù) 71
3.5.4 對(duì)偶四元數(shù) 71
3.6 本章小結(jié) 72
參考文獻(xiàn) 72
第4章 幾何與物理解釋的形式化 74
4.1 引言 74
4.2 幾何空間的表示 75
4.3 Euclidean 空間 76
4.3.1 外積零空間表示 76
4.3.2 內(nèi)積的幾何解釋 77
4.3.3 內(nèi)積零空間表示 77
4.3.4 反射 81
4.3.5 旋轉(zhuǎn) 82
4.4 射影空間 84
4.4.1 定義 84
4.4.2 外積零空間表示 85
4.4.3 內(nèi)積零空間表示 86
4.4.4 反射的表示問(wèn)題 87
4.4.5 旋轉(zhuǎn) 87
4.5 共形空間 88
4.5.1 Euclidean 空間的立體嵌入 88
4.5.2 立體嵌入的Minkowski 齊次化 89
4.5.3 G4，1的內(nèi)積零空間表示 92
4.5.4 G4，1的外積零空間表示 97
4.5.5 各種幾何實(shí)體表示方法匯總 100
4.5.6 Gn+1，1中的反射 101
4.5.7 Gn+1，1中的逆變換 102
4.5.8 Gn+1，1中的平移 105
4.5.9 Gn+1，1中的旋轉(zhuǎn) 106
4.5.10 Gn+1，1中的縮放變換 107
4.6 基本物理量的幾何代數(shù)形式化表示 108
4.6.1 質(zhì)點(diǎn)系統(tǒng)中經(jīng)典力學(xué)物理量 108
4.6.2 旋轉(zhuǎn)系統(tǒng)與剛體運(yùn)動(dòng) 109
4.7 本章小結(jié) 119
參考文獻(xiàn) 119
第5章 應(yīng)用案例 120
5.1 一種單目相機(jī)姿態(tài)估計(jì)模型的形式化分析 120
5.1.1 引言 120
5.1.2 分析方法 121
5.1.3 逆變換相機(jī)模型的形式化 121
5.1.4 透鏡畸變相機(jī)的形式化分析 123
5.1.5 反射相機(jī)的形式化分析 126
5.1.6 姿態(tài)估計(jì)的形式化 128
5.2 對(duì)稱(chēng)陀螺運(yùn)動(dòng)的形式化分析 130
5.2.1 引言 131
5.2.2 動(dòng)能和角動(dòng)量 131
5.2.3 歐拉方程與守恒定理 132
5.2.4 運(yùn)動(dòng)分析 134
5.3 本章小結(jié) 135
參考文獻(xiàn) 136
第6章 總結(jié)和展望 138
6.1 總結(jié) 138
6.2 展望 139
書(shū)單推薦
