內容簡介
《哈密頓力學理論的形式化與機器人動力學形式化分析》繫統深入地研究了辛幾何理論、哈密頓動力學的公理化體繫，並以四自由度串聯機器人為例，研究了基於哈密頓動力學繫統的形式化分析與驗證方法的應用，為機器人動力學的安全設計提供了形式化驗證理論和技術手段。《哈密頓力學理論的形式化與機器人動力學形式化分析》主要內容包括：哈密頓模型的幾何基礎——辛流形空間的形式化、哈密頓模型和拉格朗日模型的勒讓德映射關繫的形式化、哈密頓方程的形式化和機器人動力學的形式化建模與分析。內容涉及交互式定理證明、機器人、形式化驗證等人工智能領域。
目錄
目錄
序
前言
第1章緒論1
1.1研究意義1
1.2研究現狀3
1.2.1分析力學3
1.2.2形式化數學4
1.2.3機器人形式化驗證6
1.3主要內容和貢獻7
1.3.1主要研究內容7
1.3.2主要貢獻9
1.4本書組織結構9
1.5交互式定理證明器HOL Light10
參考文獻11
第2章辛幾何形式化16
2.1辛向量空間的形式化16
2.1.1辛空間與歐氏空間的異同17
2.1.2辛內積形式化定義與性質形式化證明17
2.1.3辛向量空間的形式化建模與驗證19
2.1.4辛空間基底性質形式化證明20
2.2辛變換矩陣的形式化23
2.2.1辛變換的形式化定義及其判定定理的證明策略23
2.2.2分塊矩陣相關理論的形式化25
2.2.3單位辛矩陣性質的形式化29
2.3辛群的形式化30
2.3.1辛群形式化建模31
2.3.2辛群判定定理及其證明策略32
2.4本章小結36
參考文獻36
第3章勒讓德變換形式化38
3.1勒讓德變換原理38
3函數勒讓德變換形式化模型及固有屬性的證明策略41
3函數勒讓德變換的形式化建模44
3.3.1完全勒讓德變換的形式化模型及固有屬性證明策略44
3.3.2部分勒讓德變換的形式化模型及固有屬性證明策略49
3.4本章小結58
參考文獻58
第4章哈密頓力學繫統形式化59
4.1哈密頓函數的形式化建模60
4.1.1構造力學函數數據類型60
4.1.2從拉格朗日函數到哈密頓函數形式化模型的構建63
4.1.3哈密頓函數物理意義的形式化驗證67
4.2哈密頓正則方程的形式化建模70
4.2.1哈密頓函數微分相關定理形式化描述70
4.2.2哈密頓正則方程的形式化建模及證明策略73
4.3泊松括號與泊松定理的形式化87
4.3.1泊松括號形式化描述及其性質形式化證明87
4.3.2泊松定理形式化驗證94
4.4本章小結96
參考文獻96
第5章串聯機器人哈密頓動力學形式化建模與驗證98
5.1SCARA四自由度機器人哈密頓函數形式化建模98
5.2SCARA四自由度機器人哈密頓正則方程形式化建模105
5.3機器人動力學形式化建模與驗證過程111
5.4本章小結123
參考文獻123
第6章總結與展望125
6.1主要工作和創新點125
6.2下一步工作與展望126
