目錄　 \n
序 \n
前言　 \n
第1章　緒論　1　 \n
1.1　背景　1　 \n
1.2　泛函變分、動力學(xué)與形式化驗證　2　 \n
1.2.1　泛函變分與動力學(xué)　2　 \n
1.2.2　形式化數(shù)學(xué)　3　 \n
1.2.3　形式化驗證　5　 \n
1.3　本書研究內(nèi)容　6　 \n
1.4　本書結(jié)構(gòu)　7　 \n
參考文獻(xiàn)　9　 \n
第2章　預(yù)備知識　13　 \n
2.1　泛函變分主要理論　13　 \n
2.2　拉格朗日力學(xué)主要理論　15　 \n
2.3　機(jī)器人動力學(xué)主要理論　16　 \n
2.4　形式化驗證　19　 \n
2.5　本章小結(jié)　21　 \n
參考文獻(xiàn)　21　 \n
第3章　泛函變分主要理論的形式化　23　 \n
3.1　泛函Fréchet形式變分主要理論的形式化　23　 \n
3.1.1　泛函Fréchet形式變分的形式化建模與證明策略　23　 \n
3.1.2　泛函連續(xù)與變分之間關(guān)系的形式化驗證　31　 \n
3.1.3　變分中值定理的形式化表示及證明策略　34　 \n
3.1.4　泛函Fréchet形式變分駐值條件的形式化表示及證明策略　37　 \n
3.2　泛函Gateaux形式變分主要理論的形式化建模與驗證　40　 \n
3.2.1　泛函Gateaux形式變分的形式化表示　40　 \n
3.2.2　積分型泛函Gateaux形式變分的形式化證明　42　 \n
3.2.3　泛函Gateaux形式變分駐值條件的形式化證明　45　 \n
3.3　泛函歐拉方程形式化建模與驗證　46 \n
3.3.1　一些與微積分相關(guān)的定理的形式化　46　 \n
3.3.2　單變量函數(shù)高階微分的形式化表示　49　 \n
3.3.3　變分基本引理的形式化表示與證明　52　 \n
3.3.4　一些新的向量值函數(shù)與矩陣值函數(shù)的形式化表示　55　 \n
3.3.5　泛函的歐拉方程形式化建模與驗證　60　 \n
3.4　示例驗證:氣體流動的*小阻力問題　67　 \n
3.5　本章小結(jié)　69　 \n
參考文獻(xiàn)　69　 \n
第4章　拉格朗日力學(xué)主要理論的形式化　70　 \n
4.1　哈密頓變分原理的形式化　70　 \n
4.2　虛功原理的形式化　72　 \n
4.3　達(dá)朗貝爾原理的形式化　77　 \n
4.4　一般形式拉格朗日方程的形式化　78　 \n
4.5　示例驗證:珠子沿著螺旋線運動問題　90　 \n
4.6　本章小結(jié)　94　 \n
參考文獻(xiàn)　94　 \n
第5章　機(jī)器人動力學(xué)的形式化建模與分析　95　 \n
5.1　剛體運動齊次變換的形式化表示　95　 \n
5.2　剛體速度的形式化表示　100　 \n
5.3　機(jī)器人雅可比矩陣的形式化表示　119　 \n
5.4　機(jī)器人拉格朗日方程的形式化表示　125　 \n
5.5　示例驗證：三關(guān)節(jié)串聯(lián)機(jī)器人動力學(xué)的形式化驗證　129　 \n
5.6　本章小結(jié)　132　 \n
參考文獻(xiàn)　132　 \n
第6章　模塊化自組織機(jī)器人對接運動學(xué)和動力學(xué)驗證　134　 \n
6.1　模塊化自組織機(jī)器人運動學(xué)與動力學(xué)設(shè)計　134　 \n
6.2　模塊化自組織機(jī)器人運動學(xué)的形式化驗證與分析　140　 \n
6.3　模塊化自組織機(jī)器人動力學(xué)的形式化驗證　148　 \n
6.4　本章小結(jié)　153　 \n
參考文獻(xiàn)　153　 \n
第7章　總結(jié)與展望　154　 \n
7.1　總結(jié)　154　 \n
7.2　展望　156