定理证明是人工智能的一个分支,它的研究目标是在计算机辅助下进行数学定理的证明。基于定理证明的形式化验证技术已经被广泛应用于数学定理的证明验证以及软件正确性验证。然而定理证明技术在工程数学中的应用还十分罕见。安全飞行控制系统在飞行控制中扮演了一个重要的角色并且被认为是飞机的“大脑”。只有该系统被验证为正确的飞机才能安全稳定的飞行。飞行控制算法是飞行控制系统的核心,它的基础是大量繁复的微积分数学推导,这些数学推导的正确性对飞行控制系统的安全性有关键性作用。欧洲曾经发生由于下降过程控制的失误导致火星着陆的失败。在直升机飞行控制数学的形式化验证方面,目前国际上是空白。本文是基于定理证明器Coq对直升机飞行控制系统中的部分数学公式的推导进行的形式化验证初步探索,主要研究内容如下:第一,对以显模型跟踪控制系统为基础的直升机自动过渡飞行控制过程进行验证。这一过程分为高度过渡和速度过渡两个方面,其中高度又分抛物线下降和指数拉平两个阶段。这两个阶段本身受相应的物理定律和控制目标约束,两者之间需要平滑的连接。下降曲线所满足的数学公式来源于在这些约束条件下的推导。我们对这一推导过程进行了形式化描述和验证。第二,对直升机舰上起飞过程及轨迹生成进行验证。该过程在时间上分为三个时间段即开始阶段,稳定上升阶段和终段,在空间上简化为忽略Y轴只考虑XOZ平面,在平面内通过初始状态和任务要求在保证轨迹平滑的情况下设定运动方程。验证过程中我们证明了几个自定义小引理。第三,对直升机着舰过程及轨迹生成进行验证。着舰比舰上起飞要困难,因为要考虑三个方面的因素即甲板尺寸有限、舰船晃动、直升机自身控制减弱。第四,Z变换形式化验证。Z变换能够把一系列实数或复数离散信号从时域转换成复频域,是控制系统中的重要分析手段。由于Coq标准库及第三方库中有关复数的定理相对缺乏,所以我们从复数形式化开始,通过欧拉公式等手段对复数进行转换和简化,然后在此基础上验证了Z变换的齐次,均匀,线性,以及复数位移性质,由此来扩展定理证明工具在系统分析方面的能力,同时为进一步形式化直升机飞控系统奠定了基础。