【出 处】：《 计算机仿真 》 CSCD 2014年第31卷第3期 289-294页,共6页

【作 者】： 康西楠 [1] ; 施智平 [1] ; 叶世伟 [2] ; 关永 [1]

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