Formalizing the Matrix Inversion Based on the Adjugate Matrix in HOL4

摘要：

　　This paper presents the formalization of the matrix inversion based on the adjugate matrix in the HOL4 system.It is very complex and difficult to formalize the adjugate matrix, which is composed of matrix cofactors.Because HOL4 is based on a simple type theory, it is difficult to formally express the sub-matrices and cofactors of an n-by-n matrix.In this paper, special n-by-n matrices are constructed to replace the (n-1)-by-(n-1) sub-matrices, in order to compute the cofactors, thereby, making it possible to formally construct aadjugate matrices.The Laplaces formula is proven and the matrix inversion based on the adjugate matrix is then inferred in HOL4.The paper also presents formal proofs of properties of the invertible matrix.

关键词： Formal verification Theorem proving Matrix inversion HOL4 Adjugate matrix

作者: Liming Li Zhiping Shi Yong Guan Jie Zhang Hongxing Wei

作者单位: Beijing Key Laboratory of Electronic System Reliability Technology,Capital Normal University, Beijin College of Information Science & Technology,Beijing University of Chemical Technology, Beijing 10002 School of Mechanical Engineering and Automation, Beihang University,Beijing 100083, China

会议类型: 国际会议

会议名称: 8th International Conference on Intelligent Information Processing(2014年IFIP智能信息处理国际会议)

会议地点: 杭州

会议语种:英文

页码: 178-186

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