@inproceedings{77cd16b8c97e4feab0131ecbcb0b1eb7,
title = "Formalizing the matrix inversion based on the adjugate matrix in HOL4",
abstract = "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 Laplace{\textquoteright}s 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.",
keywords = "Adjugate matrix, Formal verification, HOL4, Matrix inversion, Theorem proving",
author = "Liming Li and Zhiping Shi and Yong Guan and Jie Zhang and Hongxing Wei",
note = "Publisher Copyright: {\textcopyright} IFIP International Federation for Information Processing 2014.; 8th IFIP International Conference on Intelligent Information Processing, IIP 2014 ; Conference date: 17-10-2014 Through 20-10-2014",
year = "2014",
language = "英语",
series = "IFIP Advances in Information and Communication Technology",
publisher = "Springer New York LLC",
pages = "178--186",
editor = "David Leake and Uli Sattler and Zhongzhi Shi and Zhaohui Wu",
booktitle = "Intelligent Information Processing VII - 8th IFIP TC 12 International Conference, IIP 2014, Proceedings",
}