本書以幾何代數(shù)理論體系與自動定理證明思想為指導，系統(tǒng)深入地研究了幾何代數(shù)的形式化理論與公理化體系，構建了一個兼具代數(shù)推理和幾何解算能力的統(tǒng)一形式化數(shù)學定理體系，對代數(shù)與幾何從概念上進行了融合與拓展、從描述方法和運算法則上進行了綜合與歸納，為代數(shù)理論賦予了“形”的特征，為幾何理論提供了“數(shù)”的內(nèi)涵，并將其初步應用于實際物理問題的證明，內(nèi)容涵蓋了自動定理證明、機器人、形式化驗證等人工智能領域。全書主要內(nèi)容包括：幾何代數(shù)理論的進展、形式化理論；HOLLight定理證明器體系；幾何代數(shù)結構的形式化；幾何與物理解釋的形式化；單目相機姿態(tài)估計模型的形式化分析、對稱陀螺運動的形式化分析等初步應用案例。作者長期對系統(tǒng)形式化與自動定理證明進行深入研究，并在機器人安全驗證等領域持續(xù)實踐迭代，本書是對該過程成果的高度凝練與系統(tǒng)總結。
更多科學出版社服務，請掃碼獲取。
目錄
序
前言
第1章 緒論 1
1.1 背景 1
1.2 幾何代數(shù)與數(shù)學形式化 2
1.2.1 幾何代數(shù)的發(fā)展歷史 2
1.2.2 數(shù)學理論形式化及其發(fā)展歷史 4
1.3 主要內(nèi)容 11
1.4 本書結構 13
1.5 符號約定 14
參考文獻 15
第2章 幾何代數(shù)簡介 22
2.1 二次型空間 22
2.2 結構、元素、運算和子空間 23
2.2.1 公理性質(zhì) 23
2.2.2 幾何代數(shù)基底 24
2.2.3 多重向量 27
2.2.4 內(nèi)積和外積 27
2.3 幾何解釋 29
參考文獻 32
第3章 幾何代數(shù)結構的形式化 33
3.1 元素與運算 33
3.1.1 多重向量 34
3.1.2 積運算 39
3.1.3 幾何積的逆運算 41
3.1.4 運算性質(zhì)和自動解算程序 42
3.2 Blade 的定義及性質(zhì) 47
3.2.1 定義 47
3.2.2 幾何積 48
3.2.3 外積 49
3.2.4 線性相關 51
3.2.5 標量積 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 對偶 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ù)實例 69
3.5.1 Gibbs 向量代數(shù) 69
3.5.2 復數(shù) 70
3.5.3 四元數(shù) 71
3.5.4 對偶四元數(shù) 71
3.6 本章小結 72
參考文獻 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 反射的表示問題 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 各種幾何實體表示方法匯總 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ì)點系統(tǒng)中經(jīng)典力學物理量 108
4.6.2 旋轉(zhuǎn)系統(tǒng)與剛體運動 109
4.7 本章小結 119
參考文獻 119
第5章 應用案例 120
5.1 一種單目相機姿態(tài)估計模型的形式化分析 120
5.1.1 引言 120
5.1.2 分析方法 121
5.1.3 逆變換相機模型的形式化 121
5.1.4 透鏡畸變相機的形式化分析 123
5.1.5 反射相機的形式化分析 126
5.1.6 姿態(tài)估計的形式化 128
5.2 對稱陀螺運動的形式化分析 130
5.2.1 引言 131
5.2.2 動能和角動量 131
5.2.3 歐拉方程與守恒定理 132
5.2.4 運動分析 134
5.3 本章小結 135
參考文獻 136
第6章 總結和展望 138
6.1 總結 138
6.2 展望 139
書單推薦
