哈密頓力學理論的形式化與機器人動力學形式化分析

目錄 \n
序 \n
前言 \n
第1章緒論1 \n
1.1研究意義1 \n
1.2研究現(xiàn)狀3 \n
1.2.1分析力學3 \n
1.2.2形式化數(shù)學4 \n
1.2.3機器人形式化驗證6 \n
1.3主要內(nèi)容和貢獻7 \n
1.3.1主要研究內(nèi)容7 \n
1.3.2主要貢獻9 \n
1.4本書組織結構9 \n
1.5交互式定理證明器HOL Light10 \n
參考文獻11 \n
第2章辛幾何形式化16 \n
2.1辛向量空間的形式化16 \n
2.1.1辛空間與歐氏空間的異同17 \n
2.1.2辛內(nèi)積形式化定義與性質(zhì)形式化證明17 \n
2.1.3辛向量空間的形式化建模與驗證19 \n
2.1.4辛空間基底性質(zhì)形式化證明20 \n
2.2辛變換矩陣的形式化23 \n
2.2.1辛變換的形式化定義及其判定定理的證明策略23 \n
2.2.2分塊矩陣相關理論的形式化25 \n
2.2.3單位辛矩陣性質(zhì)的形式化29 \n
2.3辛群的形式化30 \n
2.3.1辛群形式化建模31 \n
2.3.2辛群判定定理及其證明策略32 \n
2.4本章小結36 \n
參考文獻36 \n
第3章勒讓德變換形式化38 \n
3.1勒讓德變換原理38 \n
3.2一元函數(shù)勒讓德變換形式化模型及固有屬性的證明策略41 \n
3.3多元函數(shù)勒讓德變換的形式化建模44 \n
3.3.1完全勒讓德變換的形式化模型及固有屬性證明策略44 \n
3.3.2部分勒讓德變換的形式化模型及固有屬性證明策略49 \n
3.4本章小結58 \n
參考文獻58 \n
第4章哈密頓力學系統(tǒng)形式化59 \n
4.1哈密頓函數(shù)的形式化建模60 \n
4.1.1構造力學函數(shù)數(shù)據(jù)類型60 \n
4.1.2從拉格朗日函數(shù)到哈密頓函數(shù)形式化模型的構建63 \n
4.1.3哈密頓函數(shù)物理意義的形式化驗證67 \n
4.2哈密頓正則方程的形式化建模70 \n
4.2.1哈密頓函數(shù)微分相關定理形式化描述70 \n
4.2.2哈密頓正則方程的形式化建模及證明策略73 \n
4.3泊松括號與泊松定理的形式化87 \n
4.3.1泊松括號形式化描述及其性質(zhì)形式化證明87 \n
4.3.2泊松定理形式化驗證94 \n
4.4本章小結96 \n
參考文獻96 \n
第5章串聯(lián)機器人哈密頓動力學形式化建模與驗證98 \n
5.1SCARA四自由度機器人哈密頓函數(shù)形式化建模98 \n
5.2SCARA四自由度機器人哈密頓正則方程形式化建模105 \n
5.3機器人動力學形式化建模與驗證過程111 \n
5.4本章小結123 \n
參考文獻123 \n
第6章總結與展望125 \n
6.1主要工作和創(chuàng)新點125 \n
6.2下一步工作與展望126