第1章绪论
1.1研究意义
动力学是经典物理学的基石之一，主要研究能量、力以及它们与物体的平衡、变形或运动的关系，同时也是很多数学理论的发源地。动力学问题在自然界和工程实践中无处不在，是许多工程学科的理论基础。诸如，航空航天、机器人、火车、武器等所有与运动和力相关的学科和工业都以动力学为基础[1]。
动力学主要包括牛顿力学、拉格朗日力学和哈密顿力学三个体系。牛顿力学又称矢量力学，求解时需已知所有作用力的大小、方向以及作用点与刚体质心的位置关系，因此很难建模复杂的动力学系统。拉格朗日力学则是将力学体系从以力为基本概念的矢量力学形式，改变为以能量为基本概念的标量分析力学形式，奠定了分析力学的基础，为把力学理论推广应用到物理学其他领域开辟了道路。哈密顿力学研究以 “正则变量 ”描述力学系统的运动规律，该理论体系能够发展出多种变换理论和积分方法，并在其他物理学诸如电磁波、热扩散、量子力学和相对论等重要理论领域均有广泛应用，同时架起了从经典力学到近代物理学的桥梁。
关于动力学问题的研究，通常通过分析、简化、抽象成物理模型，再建立动力学方程，即动力学建模，然后分析动力学方程的解及其性质，最后通过工程实现成为动力学系统。基于以上分析，在设计实现一个经典的动力学系统时，如何保障它的动力学建模、分析求解和设计实现的正确性和可靠性呢？传统的动力学建模与分析方法主要包括纸笔演算、数值计算和计算机代数系统。纸笔演算的方法耗时耗力，容易引入人为错误 [2]；计算机数值计算方法指利用计算机软件进行动力学的数值计算，这样的软件包括 Maple、Mathmetica、MATLAB等，但它们只能给出待解问题的数值解，无法给出问题的内在逻辑性质；计算机代数系统比如 Mathmetica能够高效进行符号代数运算，但是边界条件、奇异表达简化方面的处理具有缺陷，此外庞大的符号计算程序也不能排除程序漏洞的存在。
机器人是动力学分析与建模的典型应用，动力学分析是机器人设计和控制的中间桥梁，动力学系统的建模与设计的错误可能导致灾难性后果。未来的世界是人机共处的世界，机器人在为人类带来巨大便利的同时也带来了安全隐患。作为能够自主运动的机器，机器人故障引发的事故时有发生。 1978年 9月，日本广岛一间工厂的切割机器人将一名值班工人当作钢板切割造成惨案 [3]；2014年 1月，嫦娥三号玉兔月球车因机构控制出现故障而一度进入休眠 [4]；2015年 7月 1日，一名 22岁的技术工在大众汽车包纳塔尔工厂中被一台机器人意外伤害致死 [5]； 2016年 11月 18日在第十八届中国国际高新技术成果交易会，有一台服务机器人突然发生故障，在没有指令的前提下打砸展台玻璃，导致部分展台破坏，同时有路人受伤 [5，6]。2018年 9月 10日上午，芜湖经济开发区内一企业员工在给搬运机器人换刀具时，被突然启动的机器人夹住，虽被救下送医，但因伤势过重，不治身亡。2018年 12月 5日，美国新泽西州的亚马逊仓库一个自动化机器人意外刺穿喷雾罐发生一起防熊喷雾泄漏事故，事故导致有 24人被送医院救治。机器人安全隐患已经成为机器人特别是人机交互机器人应用普及的巨大障碍。人们开始意识到传统的测试仿真等验证方法已经不能满足安全攸关机器人的正确性、安全性验证要求 [7，8]。
传统的动力学验证主要基于测试与仿真方法，由于测试用例与仿真用例受限，测试与仿真方法均无法完全覆盖所有可能验证路径，所以，这些传统的非完备性验证手段已经无法满足安全攸关系统的动力学设计对正确性和安全性的要求。而定理证明形式化验证方法是一种完备的验证手段，可以发现传统方法难于发现的系统缺陷，能够提高整个系统的安全性和鲁棒性验证质量。
以精确和完备性为主要优点的形式化验证方法逐渐成为安全攸关系统正确性验证的重要手段，并在计算机软硬件验证中取得成功 [9-11]。近年来，通过形式化验证技术提升机器人的正确性和安全性逐渐成为研究热点 [12-14]。一些国际上广泛认可的安全标准如 IEC61508等将形式化验证作为达到高安全等级的必选项 [15]。 2011年，美国国家科学基金会提出未来重点支持与人协作机器人的研究工作，而且如何保障与人协作的安全性是研究重点。 2013年，美国政府发布 A Roadmap for U.S. Robotics的白皮书，提出未来五十年发展重点将从因特网转移到机器人产业 [16]，并第一次提出了将形式化验证方法应用于可靠性、安全性高的机器人领域。因此，把动力学的建模和分析求解过程用数理逻辑表示，并进行严格的推理和证明，能够最大限度地确保系统设计的正确性和可靠性。
数学理论的形式化是指用数理逻辑语言描述或建模数学理论，包括数学概念的形式化定义、定理的形式化表示和证明。使用定理证明的基础是数学理论的逻辑表示—–形式化数学，国际上主流的定理证明器，如 HOL4[17]、HOL Light[18-20]、 Isabella/HOL [21]、COQ[22]、PVS [23，24]等，均包含了很多基础的数学理论逻辑程序库，比如集合论、实分析、向量代数、矩阵理论等，但是目前还没有与动力学理论相关的公理化体系和定理库，这就严重制约了机器证明在机器人动力系统、导航、自动控制等领域的广泛应用。
建立动力学的形式化理论定理证明库是动力系统形式化建模与分析的基础。基于辛几何理论的哈密顿力学是系统动力学分析的重要工具之一 [25]。辛几何理论不仅使求解更方便，而且物理意义清晰明确，在科学研究和工程实践中得到广泛应用。
综上所述，基于形式化数学的定理证明方法在机器人和计算机等安全攸关系统的设计验证中具有重要的理论意义和应用价值。鉴于此，本书聚焦动力学理论的形式化建模和证明理论的研究，设计实现哈密顿动力学的高阶逻辑定理库，为动力学系统的形式化分析与验证提供方法和工具支持。
1.2研究现状
本书主要研究哈密顿动力学的高阶逻辑形式化及其在机器人动力学系统形式化验证中的应用，因此本节将从分析力学、形式化数学以及机器人形式化验证等几个方面介绍研究发展的历程和现状。
1.2.1分析力学
分析力学以广义坐标为描述质点系的变量，以最小作用原理为基石，发展了虚位移原理和达朗贝尔原理，运用数学分析方法研究宏观现象中的力学问题。近 20年来，又发展出用近代微分几何的观点来研究非平直空间的流形上连续变量和高度非线性力学的原理和方法。它广泛用于结构分析、机器动力学与振动、航天力学、多刚体系统和机器人动力学等工程技术领域，也可推广应用于连续介质力学和相对论力学 [26，27]。分析力学是适合于研究宏观现象的力学体系，研究对象是刚体或质点系。它阐述了力学的普遍原理，由这些原理出发导出质点系的基本运动微分方程，并研究这些方程本身以及它们的积分方法。质点系可视为宏观物体组成的力学系统的理想模型，如刚体、弹性体、流体以及它们的综合体都可看作质点系，质点数可由一到无穷。工程上的力学问题大多数是约束的质点系，由于约束方程类型的不同，从而形成了不同的力学系统。分析力学分为拉格朗日力学和哈密顿力学 [28，29]。前者以拉格朗日量刻画力学系统，其运动方程称为拉格朗日方程；后者以哈密顿量刻画力学系统，其运动方程为哈密顿正则方程。由拉格朗日和哈密顿所奠基的分析力学是一门已经成熟发展了的学科。和目前兴起的种种新学科相比，它确实显得传统，但由于其可准确、深刻地描述现存物理学的动力学本质，所以其价值还在与日俱增。
拉格朗日是分析力学的创立者，在其名著《分析力学》中 ，他发展了达朗贝尔和欧拉等人的研究成果，建立起拉格朗日方程，把力学体系的运动方程从以力为基本概念的牛顿形式，转变为以能量为基本概念的分析力学形式 [30，31]，为现代动力学理论的发展奠定了基础，也对近代数学和物理学发展起到了巨大的推动作用。利用拉格朗日第一类方程解决系统的动力学问题，与矢量动力学的一般方法一样，尽管建立方程比较容易，但其求解规模很大。拉格朗日第二类方程从独立坐标出发，利用纯数学分析方法，将用独立坐标描述的动力学方程用统一的原理与公式进行表达，克服了在矢量动力学中建立这种方程依赖技巧的缺点，但此时建立的拉格朗日方程是一个多维二阶偏微分方程，求解难度相对较大。同时，方程中的拉格朗日函数表示动能与势能之差，虽具有能量量纲，但却存在物理意义并不明确的不足。
哈密顿体系在多维位置和动量 (p， q)构成的相空间即辛空间中研究完整系统的力学问题，把分析力学推进一步。 1843年，哈密顿推得的用广义坐标和广义动量联合表示的动力学方程，称为正则方程 [32]。哈密顿正则方程将拉格朗日方程由 n个二阶偏微分方程降阶为 2n个一阶的偏微分方程，求解规模与难度下降显著。另外，方程中的哈密顿函数表示动能与势能之和，即表示系统的机械能，因此，物理意义更加清晰。1894年，赫兹提出将约束和系统分成完整的和非完整的两大类，从此开始非完整系统分析力学的研究。经典力学基本定理用辛几何的语言就表示为 “一切哈密顿体系的动力演化都使辛度量保持不变，即都是辛正则变换 ” [33-35]。 1984年，冯康在微分几何和微分方程国际会议上发表的论文《差分格式与辛几何》[36，37]，首次系统地提出哈密顿方程和哈密顿算法，提出从辛几何内部系统构成算法来研究其性质的途径，从而开创了哈密顿算法这一新领域，这是计算物理、计算力学和计算数学相互结合渗透的前沿领域。
1.2.2形式化数学
数学以精确的语言和清晰的论证规则著称，被认为是可以自证正确性的科学，但是数学论著中的错误却不在少数 [38]。Lecat在 1935年发表的书中用 130页的篇幅汇集了 1900年以前主要数学家犯的错误； 1879年发表的四色定理的第一个证明于十年后发现是错误的； Wiles关于费马大定理的证明被审稿人发现有错误，Wiles和学生花了一年时间来纠正； 1998年，Hales关于开普勒猜想的证明长达 300页和 4万行计算机代码 (非形式化代码 )，数学领域顶级期刊 Annals of Mathematics委托 12位审稿人用整整 4年时间审阅证明，最后只给出 99%可能是正确的结论，主编非常担忧，认为这样的情况会越来越多 [39]。形式化数学通过计算机对数学理论进行形式化描述，可以对数学证明的正确性进行检查和验证，确保数学证明本身的正确性，同时可以建立一个包含数学定义、定理和证明的形式化数学库 [40，41]作为证明新理论的工作基础。
形式化数学的核心主要包括逻辑语言、证明工具和形式化数学库三部分 [42]。 Wiedijk[43]认为，形式化数学是数学发展历史上的第三次革命。形式化数学可以帮助数学家检查证明的正确性，从而构建更加可靠的数学理论，同时也构建了计算机可以理解的数学知识库。它不仅是机器定理证明的基础，同时也是计算机软硬件系统形式化验证的基础，因此，形式化数学已经成为基础科学的重要研究领域。
形式化数学早期最著名的案例是 1996年 McCune使用完全自动定理证明器 EQP给出了 Robbins猜想的机器证明 [39]。
