A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem
-
1
Universidad de La Rioja
info
ISSN: 0168-7433
Argitalpen urtea: 2017
Alea: 58
Zenbakia: 4
Orrialdeak: 509-535
Mota: Artikulua
beta Ver similares en nube de resultadosBeste argitalpen batzuk: Journal of Automated Reasoning
Lotura duten proiektuak
Laburpena
In this paper we show how a thoughtful reusing of libraries can provide concise proofs of non-trivial mathematical results. Concretely, we formalise in Isabelle/HOL a proof of the Fundamental Theorem of Linear Algebra for vector spaces over inner product spaces, the Gram–Schmidt process of orthogonalising vectors over (Formula presented.), its application to get the (Formula presented.) decomposition of a matrix, and the least squares approximation of systems of linear equations without solution, in a modest number of lines (ca. 2700). This work intensively reuses previous results, such as the Rank–Nullity theorem and various applications of the Gauss–Jordan algorithm. The formalisation is also accompanied by code generation and refinements that enable the execution of the presented algorithms in Isabelle and SML. © 2016 Springer Science+Business Media Dordrecht