希尔伯特空间以及矩阵理论在HOL4中的形式化

定理证明方法可以用于任何能被数学模型表示的系统，不受状态数限制，是非常理想的验证方法，而定理库的构建是定理证明应用的关键问题。矩阵是线性变换的算子，在信息系统中应用广泛。在定理证明器中系统地构建矩阵理论和线性变换理论将会极大地提高定理证明器的建模和推理能力。本项目研究有限维希尔伯特空间以及矩阵理论的形式化方法，研究线性变换性质的形式化方法，包括相关性、对称性、正交性和同构性，并在高阶逻辑定理证明环境HOL4中开发相应的定理库，构建以矩阵理论为核心的定理证明体系，在国际上公开发布HOL4矩阵定理库，推动HOL4在时间状态变换和空间变换系统的验证中的应用，提高我国在定理证明基础平台构建领域的国际影响力。基于所研发的矩阵定理库，用定理证明方法验证SpaceWire总线的发送接收、编码模块和总线控制模块，示范矩阵定理库的应用。

本项目研究希尔伯特空间理论的形式化并基于HOL定理证明器开发了希尔伯特高阶逻辑定理库，包括代数系统、复数理论、矩阵理论、gauge积分、内积空间、傅里叶变换、拉普拉斯变换、分数阶分析理论、旋量理论等的形式化，其中复数定理库和gauge积分定理库已经被剑桥大学HOL官方组织所接受，分别在HOL4 Kananaskis-7和Kananaskis-9版本中发布；在希尔伯特空间形式化理论的基础之上，我们研究旋量代数的形式化理论，开发了旋量理论的高阶逻辑定理库，基于旋量理论提出了机器人运动学形式化分析与验证理论。对空间串行通讯总线SpaceWire的8个模块进行了系统的形式化验证，并发现其中的3处代码缺陷，提高了SpaceWire总线系统的正确性。本项目研发的希尔伯特空间形式化理论为线性系统的形式化分析与验证奠定了基础，在国际上首次实现旋量理论的形式化，和机器人运动学形式化分析与验证方法。