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.
Chapter PDF
Similar content being viewed by others
References
Harrison, J.V.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114–129. Springer, Heidelberg (2005)
Robert, C., Solovay, M., Arthan, R.D., Harrison, J.: Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904.3482, Submitted to the Annals of Pure and Applied Logic (2009)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)
Nakamura, Y., Tamura, N., Chang, W.: A Theory of Matrices of Real Elements. J. Formalized Mathematics 14(1), 21–28 (2006)
Tamura, N., Nakamura, Y.: Determinant and Inverse of Matrices of Real Elements. J. Formalized Mathematics 15(3), 127–136 (2007)
Obua, S.: Proving bounds for real linear programs in isabelle/HOL. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 227–244. Springer, Heidelberg (2005)
Pasca, I.: Formal Proofs for Theoretical Properties of Newton’s Method. Rapport de recherché INRIA Sophia Antipolis, 28 pages (February 2010)
Paşca, I.: Formally verified conditions for regularity of interval matrices. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 219–233. Springer, Heidelberg (2010)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press (1986)
Church, A.: A formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940)
Diaconescu, R.: Axiom of choice and complementation. Proceedings of the American Mathematical Society 51, 176–178 (1975)
Gordon, M.J.C.: Representing a logic in the LCF metalanguage. In: Néel, D. (ed.) Tools and notions for program construction: an advanced course, pp. 163–185. Cambridge University Press (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Li, L., Shi, Z., Guan, Y., Zhang, J., Wei, H. (2014). Formalizing the Matrix Inversion Based on the Adjugate Matrix in HOL4. In: Shi, Z., Wu, Z., Leake, D., Sattler, U. (eds) Intelligent Information Processing VII. IIP 2014. IFIP Advances in Information and Communication Technology, vol 432. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44980-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-662-44980-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44979-0
Online ISBN: 978-3-662-44980-6
eBook Packages: Computer ScienceComputer Science (R0)