●序
前言
第1章 緒論
1.1 背景
1.2 幾何代數與數學形式化
1.2.1 幾何代數的發展歷史
1.2.2 數學理論形式化及其發展歷史
1.3 主要內容
1.4 本書結構
1.5 符號約定
參考文獻
第2章 幾何代數簡介
2.1 二次型空間
2.2 素、運算和子空間
2.2.1 公理性質
2.2.2 幾何代數基底
2.2.3 多重向量
2.2.4 內積和外積
2.3 幾何解釋
參考文獻
第3章 幾何代數結構的形式化
3素與運算
3.1.1 多重向量
3.1.2 積運算
3.1.3 幾何積的逆運算
3.1.4 運算性質和自動解算程序
3.2 Blade 的定義及性質
3.2.1 定義
3.2.2 幾何積
3.2.3 外積
3.2.4 線性相關
3.2.5 標量積
3.2.6 反轉
3.2.7 共軛
3.2.8 範數
3.2.9 內積
3.2.10 對偶
3.2.11 逆和偽逆
3.2.12 水平投影
3.2.13 垂直投影
3.2.14 相交和連接
3.3 Versor 的定義及性質
3.3.1 定義
3.3.2 性質
3.3.3 幾何變換
3.4 多重向量的微分
3.5 具體代數實例
3.5.1 Gibbs 向量代數
3.5.2 復數
3.5.數
3.5.4 數
3.6 本章小結
參考文獻
第4章 幾何與物理解釋的形式化
4.1 引言
4.2 幾何空間的表示
4.3 Euclidean 空間
4.3.1 外積零空間表示
4.3.2 內積的幾何解釋
4.3.3 內積零空間表示
4.3.4 反射
4.3.5 旋轉
4.4 射影空間
4.4.1 定義
4.4.2 外積零空間表示
4.4.3 內積零空間表示
4.4.4 反射的表示問題
4.4.5 旋轉
4.5 共形空間
4.5.1 Euclidean 空間的立體嵌入
4.5.2 立體嵌入的Minkowski 齊次化
4.5.3 G4,1的內積零空間表示
4.5.4 G4,1的外積零空間表示
4.5.5 各種幾何實體表示方法彙總
4.5.6 Gn+1,1中的反射
4.5.7 Gn+1,1中的逆變換
4.5.8 Gn+1,1中的平移
4.5.9 Gn+1,1中的旋轉
4.5.10 Gn+1,1中的縮放變換
4.6 基本物理量的幾何代數形式化表示
4.6.1 質點繫統中經典力學物理量
4.6.2 旋轉繫統與剛體運動
4.7 本章小結
參考文獻
第5章 應用案例
5.1 一種單目相機姿態估計模型的形式化分析
5.1.1 引言
5.1.2 分析方法
5.1.3 逆變換相機模型的形式化
5.1.4 透鏡畸變相機的形式化分析
5.1.5 反射相機的形式化分析
5.1.6 姿態估計的形式化
5.2 對稱陀螺運動的形式化分析
5.2.1 引言
5.2.2 動能和角動量
5.2.3 歐拉方程與守恆定理
5.2.4 運動分析
5.3 本章小結
參考文獻
第6章 總結和展望
6.1 總結
6.2 展望

本書以幾何代數理論體繫與自動定理證明思想為指導，繫統深入地研究了幾何代數的形式化理論與公理化體繫，構建了一個兼具代數推理和幾何解算能力的統一形式化數學定理體繫，對代數與幾何從概念上進行了融合與拓展、從描述方法和運算法則上進行了綜合與歸納，為代數理論賦予了“形”的特征，為幾何理論提供了“數”的內涵，並將其初步應用於實際物理問題的證明，內容涵蓋了自動定理證明、機器人、形式化驗證等人工智能領域。全書主要內容包括：幾何代數理論的進展、形式化理論； HOL Light定理證明器體繫；幾何代數結構的形式化幾何與物理解釋的形式化：單目相機姿態估計模型的形式化分析、對稱陀螺運動的形式化分析等初步應用案例。作者長期對繫統形式化與白動定理證明進行深入研究，並在機器人安全驗證等領域持續實踐迭代，本書是對該過程成果的高度凝練與繫統總結本書可作為人工智能、自動定理證明、機器人學、形式化驗證、數學、計算機及軟件等領域等