●序
前言
第1章 緒論
1.1 研究意義
1.2 研究現狀
1.2.1 分析力學
1.2.2 形式化數學
1.2.3 機器人形式化驗證
1.3 主要內容和貢獻
1.3.1 主要研究內容
1.3.2 主要貢獻
1.4 本書組織結構
1.5 交互式定理證明器HOL Light
參考文獻
第2章 辛幾何形式化
2.1 辛向量空間的形式化
2.1.1 辛空間與歐氏空間的異同
2.1.2 辛內積形式化定義與性質形式化證明
2.1.3 辛向量空間的形式化建模與驗證
2.1.4 辛空間基底性質形式化證明
2.2 辛變換矩陣的形式化
2.2.1 辛變換的形式化定義及其判定定理的證明策略
2.2.2 分塊矩陣相關理論的形式化
2.2.3 單位辛矩陣性質的形式化
2.3 辛群的形式化
2.3.1 辛群形式化建模
2.3.2 辛群判定定理及其證明策略
2.4 本章小結
參考文獻
第3章 勒讓德變換形式化
3.1 勒讓德變換原理
3.函數勒讓德變換形式化模型及固有屬性的證明策略
3.函數勒讓德變換的形式化建模
3.3.1 接近勒讓德變換的形式化模型及固有屬性證明策略
3.3.2 部分勒讓德變換的形式化模型及固有屬性證明策略
3.4 本章小結
參考文獻
第4章 哈密頓力學繫統形式化
4.1 哈密頓函數的形式化建模
4.1.1 構造力學函數數據類型
4.1.2 從拉格朗日函數到哈密頓函數形式化模型的構建
4.1.3 哈密頓函數物理意義的形式化驗證
4.2 哈密頓正則方程的形式化建模
4.2.1 哈密頓函數微分相關定理形式化描述
4.2.2 哈密頓正則方程的形式化建模及證明策略
4.3 泊松括號與泊松定理的形式化
4.3.1 泊松括號形式化描述及其性質形式化證明
4.3.2 泊松定理形式化驗證
4.4 本章小結
參考文獻
第5章 串聯機器人哈密頓動力學形式化建模與驗證
5.1 SCARA四自由度機器人哈密頓函數形式化建模
5.2 SCARA四自由度機器人哈密頓正則方程形式化建模
5.3 機器人動力學形式化建模與驗證過程
5.4 本章小結
參考文獻
第6章 總結與展望
6.1 主要工作和創新點
6.2 下一步工作與展望

本書繫統深入地研究了辛幾何理論、哈密頓動力學的公理化體繫，並以四自由度串聯機器人為例，研究了基於哈密頓動力學繫統的形式化分析與驗證方法的應用，為機器人動力學的安全設計提供了形式化驗證理論和技術手段。全書主要內容包括：哈密頓模型的幾何基礎——辛流形空間的形式化、哈密頓模型和拉格朗日模型的勒讓德映射關繫的形式化、哈密頓方程的形式化和機器人動力學的形式化建模與分析。內容涉及交互式定理證明、機器人、形式化驗證等人工智能領域。本書可作為機器定理證明、機器人學、形式化方法、理論計算機科學及軟件工程等領域科研人員和工程技術人員的參考書，也可作為高等院校相關專業高年級本科生和研究生的學習用書。