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

【Abstract】 Matrix is one of the most important concepts in math,and it is based on matrix transformation in Euclidean space to analysis systems which involves matrix. Theorem proving of formal verification based on math logic will be powerful for ensuring correct of systems. In order to enhance the verification ability of higher-order-logic 4( HOL4) for hardware system design,we built a matrix transformation theory library for it. We formalized definitions and properties,including elementary transformation,similarity transformation,congruent transformation,orthonormal matrix,rank of matrix,trace of matrix,eigenvalue and eigenvector. Then we used them to verify the properties of householder transformation.更多还原