哈密頓力學(xué)理論的形式化與機(jī)器人動力學(xué)形式化分析

目錄 \n
序 \n
前言 \n
第1章緒論1 \n
1.1研究意義1 \n
1.2研究現(xiàn)狀3 \n
1.2.1分析力學(xué)3 \n
1.2.2形式化數(shù)學(xué)4 \n
1.2.3機(jī)器人形式化驗(yàn)證6 \n
1.3主要內(nèi)容和貢獻(xiàn)7 \n
1.3.1主要研究內(nèi)容7 \n
1.3.2主要貢獻(xiàn)9 \n
1.4本書組織結(jié)構(gòu)9 \n
1.5交互式定理證明器HOL Light10 \n
參考文獻(xià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辛向量空間的形式化建模與驗(yàn)證19 \n
2.1.4辛空間基底性質(zhì)形式化證明20 \n
2.2辛變換矩陣的形式化23 \n
2.2.1辛變換的形式化定義及其判定定理的證明策略23 \n
2.2.2分塊矩陣相關(guān)理論的形式化25 \n
2.2.3單位辛矩陣性質(zhì)的形式化29 \n
2.3辛群的形式化30 \n
2.3.1辛群形式化建模31 \n
2.3.2辛群判定定理及其證明策略32 \n
2.4本章小結(jié)36 \n
參考文獻(xià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本章小結(jié)58 \n
參考文獻(xiàn)58 \n
第4章哈密頓力學(xué)系統(tǒng)形式化59 \n
4.1哈密頓函數(shù)的形式化建模60 \n
4.1.1構(gòu)造力學(xué)函數(shù)數(shù)據(jù)類型60 \n
4.1.2從拉格朗日函數(shù)到哈密頓函數(shù)形式化模型的構(gòu)建63 \n
4.1.3哈密頓函數(shù)物理意義的形式化驗(yàn)證67 \n
4.2哈密頓正則方程的形式化建模70 \n
4.2.1哈密頓函數(shù)微分相關(guān)定理形式化描述70 \n
4.2.2哈密頓正則方程的形式化建模及證明策略73 \n
4.3泊松括號與泊松定理的形式化87 \n
4.3.1泊松括號形式化描述及其性質(zhì)形式化證明87 \n
4.3.2泊松定理形式化驗(yàn)證94 \n
4.4本章小結(jié)96 \n
參考文獻(xiàn)96 \n
第5章串聯(lián)機(jī)器人哈密頓動力學(xué)形式化建模與驗(yàn)證98 \n
5.1SCARA四自由度機(jī)器人哈密頓函數(shù)形式化建模98 \n
5.2SCARA四自由度機(jī)器人哈密頓正則方程形式化建模105 \n
5.3機(jī)器人動力學(xué)形式化建模與驗(yàn)證過程111 \n
5.4本章小結(jié)123 \n
參考文獻(xiàn)123 \n
第6章總結(jié)與展望125 \n
6.1主要工作和創(chuàng)新點(diǎn)125 \n
6.2下一步工作與展望126