计算机仿真
計算機倣真
계산궤방진
COMPUTER SIMULATION
2014年
3期
289-294
,共6页
康西楠%施智平%叶世伟%关永
康西楠%施智平%葉世偉%關永
강서남%시지평%협세위%관영
形式化%定理证明%矩阵变换%豪斯霍尔德矩阵
形式化%定理證明%矩陣變換%豪斯霍爾德矩陣
형식화%정리증명%구진변환%호사곽이덕구진
Formalization%Theorem proving%Matrix transformation%Householder matrix
矩阵是数学中最重要的概念之一,欧氏空间上的变换理论是对涉及到矩阵的系统进行分析的基础.形式化验证中的定理证明方法基于数理逻辑,是确保系统设计正确的有力方法.使用高阶逻辑,在定理证明器HOL4中添加矩阵变换理论定理库,将会提高HOL4对涉及矩阵的系统建模和验证能力.形式化包括矩阵初等变换、矩阵相似和合同变换、矩阵正交化、矩阵的秩、矩阵的迹、特征值及特征多项式等定义和定理,并根据相关定理对豪斯霍尔德变换性质进行验证.形式化所做工作均已做成定理库.
矩陣是數學中最重要的概唸之一,歐氏空間上的變換理論是對涉及到矩陣的繫統進行分析的基礎.形式化驗證中的定理證明方法基于數理邏輯,是確保繫統設計正確的有力方法.使用高階邏輯,在定理證明器HOL4中添加矩陣變換理論定理庫,將會提高HOL4對涉及矩陣的繫統建模和驗證能力.形式化包括矩陣初等變換、矩陣相似和閤同變換、矩陣正交化、矩陣的秩、矩陣的跡、特徵值及特徵多項式等定義和定理,併根據相關定理對豪斯霍爾德變換性質進行驗證.形式化所做工作均已做成定理庫.
구진시수학중최중요적개념지일,구씨공간상적변환이론시대섭급도구진적계통진행분석적기출.형식화험증중적정리증명방법기우수리라집,시학보계통설계정학적유력방법.사용고계라집,재정리증명기HOL4중첨가구진변환이론정리고,장회제고HOL4대섭급구진적계통건모화험증능력.형식화포괄구진초등변환、구진상사화합동변환、구진정교화、구진적질、구진적적、특정치급특정다항식등정의화정리,병근거상관정리대호사곽이덕변환성질진행험증.형식화소주공작균이주성정리고.
