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

项目名称： 希尔伯特空间以及矩阵理论在HOL4中的形式化

项目编号： No.61170304

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 施智平

作者单位： 首都师范大学

项目金额： 52万元

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

中文关键词： 希尔伯特空间；gauge积分理论；矩阵理论；高阶逻辑；旋量理论

英文摘要：

英文关键词： Hilbert space；gauge integral；matrix theory；higher-order logic；screw theory