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

摘要：

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

关键词：形式化、定理证明、矩阵变换、豪斯霍尔德矩阵

所属期刊栏目：31

分类号：TP301.2(计算技术、计算机技术)

在线出版日期：2014-04-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：289-294