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

序
前言
第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.2 一元函数勒让德变换形式化模型及固有属性的证明策略
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 下一步工作与展望