●序
前言
第1章 緒論
1.1 背景
1.2 泛函變分、動力學與形式化驗證
1.2.1 泛函變分與動力學
1.2.2 形式化數學
1.2.3 形式化驗證
1.3 本書研究內容
1.4 本書結構
參考文獻
第2章 預備知識
2.1 泛函變分主要理論
2.2 拉格朗日力學主要理論
2.3 機器人動力學主要理論
2.4 形式化驗證
2.5 本章小結
參考文獻
第3章 泛函變分主要理論的形式化
3.1 泛函Frechet形式變分主要理論的形式化
3.1.1 泛函Frechet形式變分的形式化建模與證明策略
3.1.2 泛函連續與變分之間關繫的形式化驗證
3.1.3 變分中值定理的形式化表示及證明策略
3.1.4 泛函Frechet形式變分駐值條件的形式化表示及證明策略
3.2 泛函Gateaux形式變分主要理論的形式化建模與驗證
3.2.1 泛函Gateaux形式變分的形式化表示
3.2.2 積分型泛函Gateaux形式變分的形式化證明
3.2.3 泛函Gateaux形式變分駐值條件的形式化證明
3.3 泛函歐拉方程形式化建模與驗證
3.3.1 一些與微積分相關的定理的形式化
3.3.2 單變量函數高階微分的形式化表示
3.3.3 變分基本引理的形式化表示與證明
3.3.4 一些新的向量值函數與矩陣值函數的形式化表示
3.3.5 泛函的歐拉方程形式化建模與驗證
3.4 示例驗證：氣體流動的最小阻力問題
3.5 本章小結
參考文獻
第4章 拉格朗日力學主要理論的形式化
4.1 哈密頓變分原理的形式化
4.2 虛功原理的形式化
4.3 達朗貝爾原理的形式化
4.4 一般形式拉格朗日方程的形式化
4.5 示例驗證：珠子沿著螺旋線運動問題
4.6 本章小結
參考文獻
第5章 機器人動力學的形式化建模與分析
5.1 剛體運動齊次變換的形式化表示
5.2 剛體速度的形式化表示
5.3 機器人雅可比矩陣的形式化表示
5.4 機器人拉格朗日方程的形式化表示
5.5 示例驗證：三關節串聯機器人動力學的形式化驗證
5.6 本章小結
參考文獻
第6章 模塊化自組織機器人對接運動學和動力學驗證
6.1 模塊化自組織機器人運動學與動力學設計
6.2 模塊化自組織機器人運動學的形式化驗證與分析
6.3 模塊化自組織機器人動力學的形式化驗證
6.4 本章小結
參考文獻
第7章 總結與展望
7.1 總結
7.2 展望

本書以拉格朗日力學理論與自動定理證明思想為指導，繫統深入地研究了泛函變分、拉格朗日力學和機器人動力學之間的天然關繫，從而構建了以泛函變分的形式化為形式化數學基礎、以拉格朗日力學的形式化為中心、以機器人動力學形式化分析為應用依托的定理證明體繫。內容涵蓋了自動定理證明、泛函變分、拉格朗日力學、形式化驗證等領域。全書主要內容包括：泛函變分、動力學與形式化驗證的進展；泛函變分、拉格朗日力學、機器人動力學與形式化驗證主要理論；泛函變分主要理論的形式化；拉格朗日力學主要理論的形式化；機器人動力學的形式化建模與分析；模塊化自組織機器人對接運動學和動力學驗證。作者長期對繫統形式化與自動定理證明進行深入研究並在機器人安全驗證等領域持續實踐迭代，本書是對該過程成果的高度凝練與繫統總結。本書可作為從事形式化驗證、動力學、機器人動力學形式化分析研究的科研人員和工程技術人員的參考書，也可以作為高等院校相關專業高年級等