矩阵变换理论在HOL4中的形式化

摘要

矩阵是数学中最重要的概念之一,欧氏空间上的变换理论是对涉及到矩阵的系统进行分析的基础.形式化验证中的定理证明方法基于数理逻辑,是确保系统设计正确的有力方法.使用高阶逻辑,在定理证明器HOL4中添加矩阵变换理论定理库,将会提高HOL4对涉及矩阵的系统建模和验证能力.形式化包括矩阵初等变换、矩阵相似和合同变换、矩阵正交化、矩阵的秩、矩阵的迹、特征值及特征多项式等定义和定理,并根据相关定理对豪斯霍尔德变换性质进行验证.形式化所做工作均已做成定理库.