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

Formalization of Matrix Transformation Theory in HOL4

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

机构地区：[1]首都师范大学信息工程学院,北京100048 [2]中国科学院研究生院信息科学与工程学院,北京100049

出　　处：《计算机仿真》2014年第3期289-294,共6页Computer Simulation

摘　　要：矩阵是数学中最重要的概念之一,欧氏空间上的变换理论是对涉及到矩阵的系统进行分析的基础。形式化验证中的定理证明方法基于数理逻辑,是确保系统设计正确的有力方法。使用高阶逻辑,在定理证明器HOL4中添加矩阵变换理论定理库,将会提高HOL4对涉及矩阵的系统建模和验证能力。形式化包括矩阵初等变换、矩阵相似和合同变换、矩阵正交化、矩阵的秩、矩阵的迹、特征值及特征多项式等定义和定理,并根据相关定理对豪斯霍尔德变换性质进行验证。形式化所做工作均已做成定理库。Matrix is one of the most important concepts in math, and it is based on matrix transformation in Eu- clidean 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 （HOIA） 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.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]