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

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