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’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.
Type de document :
Communication dans un congrès
Zhongzhi Shi; Zhaohui Wu; David Leake; Uli Sattler. 8th International Conference on Intelligent Information Processing (IIP), Oct 2014, Hangzhou, China. Springer, IFIP Advances in Information and Communication Technology, AICT-432, pp.178-186, 2014, Intelligent Information Processing VII. 〈10.1007/978-3-662-44980-6_20〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01383331
Contributeur : Hal Ifip <>
Soumis le : mardi 18 octobre 2016 - 14:55:39
Dernière modification le : mardi 18 octobre 2016 - 15:08:50

Fichier

978-3-662-44980-6_20_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Liming Li, Zhiping Shi, Yong Guan, Jie Zhang, Hongxing Wei. Formalizing the Matrix Inversion Based on the Adjugate Matrix in HOL4. Zhongzhi Shi; Zhaohui Wu; David Leake; Uli Sattler. 8th International Conference on Intelligent Information Processing (IIP), Oct 2014, Hangzhou, China. Springer, IFIP Advances in Information and Communication Technology, AICT-432, pp.178-186, 2014, Intelligent Information Processing VII. 〈10.1007/978-3-662-44980-6_20〉. 〈hal-01383331〉

Partager

Métriques

Consultations de la notice

30

Téléchargements de fichiers

19