哈密顿力学理论的形式化与机器人动力学形式化分析

　　《哈密顿力学理论的形式化与机器人动力学形式化分析》系统深入地研究了辛几何理论、哈密顿动力学的公理化体系，并以四自由度串联机器人为例，研究了基于哈密顿动力学系统的形式化分析与验证方法的应用，为机器人动力学的安全设计提供了形式化验证理论和技术手段。《哈密顿力学理论的形式化与机器人动力学形式化分析》主要内容包括：哈密顿模型的几何基础——辛流形空间的形式化、哈密顿模型和拉格朗日模型的勒让德映射关系的形式化、哈密顿方程的形式化和机器人动力学的形式化建模与分析。内容涉及交互式定理证明、机器人、形式化验证等人工智能领域。

暂缺《哈密顿力学理论的形式化与机器人动力学形式化分析》作者简介

目录 \n
序 \n
前言 \n
第1章绪论1 \n
1.1研究意义1 \n
1.2研究现状3 \n
1.2.1分析力学3 \n
1.2.2形式化数学4 \n
1.2.3机器人形式化验证6 \n
1.3主要内容和贡献7 \n
1.3.1主要研究内容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辛内积形式化定义与性质形式化证明17 \n
2.1.3辛向量空间的形式化建模与验证19 \n
2.1.4辛空间基底性质形式化证明20 \n
2.2辛变换矩阵的形式化23 \n
2.2.1辛变换的形式化定义及其判定定理的证明策略23 \n
2.2.2分块矩阵相关理论的形式化25 \n
2.2.3单位辛矩阵性质的形式化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一元函数勒让德变换形式化模型及固有属性的证明策略41 \n
3.3多元函数勒让德变换的形式化建模44 \n
3.3.1完全勒让德变换的形式化模型及固有属性证明策略44 \n
3.3.2部分勒让德变换的形式化模型及固有属性证明策略49 \n
3.4本章小结58 \n
参考文献58 \n
第4章哈密顿力学系统形式化59 \n
4.1哈密顿函数的形式化建模60 \n
4.1.1构造力学函数数据类型60 \n
4.1.2从拉格朗日函数到哈密顿函数形式化模型的构建63 \n
4.1.3哈密顿函数物理意义的形式化验证67 \n
4.2哈密顿正则方程的形式化建模70 \n
4.2.1哈密顿函数微分相关定理形式化描述70 \n
4.2.2哈密顿正则方程的形式化建模及证明策略73 \n
4.3泊松括号与泊松定理的形式化87 \n
4.3.1泊松括号形式化描述及其性质形式化证明87 \n
4.3.2泊松定理形式化验证94 \n
4.4本章小结96 \n
参考文献96 \n
第5章串联机器人哈密顿动力学形式化建模与验证98 \n
5.1SCARA四自由度机器人哈密顿函数形式化建模98 \n
5.2SCARA四自由度机器人哈密顿正则方程形式化建模105 \n
5.3机器人动力学形式化建模与验证过程111 \n
5.4本章小结123 \n
参考文献123 \n
第6章总结与展望125 \n
6.1主要工作和创新点125 \n
6.2下一步工作与展望126