Reseña: Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL
Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL, titulada Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL.
Su autor es Jose Divasón Mallagaray, dirigido por Jesús María Aransay Azofra (de la Univ. de la Rioja).
La presentación del trabajo tuvo lugar el 25 de Octubre de 2011 en la Universidad de la Rioja.
El objetivo del trabajo es la formalización en Isabelle/HOL de conceptos y teoremas sobre álgebra lineal siguiendo la 16 primeras secciones del libro de Halmos Finite-dimensional vector spaces.
El resumen del trabajo es
In this work we deal with finite-dimensional vector spaces over a generic field
. First we will state properties of vector spaces independently of their dimension. Then, we will introduce the conditions to obtain finite-dimensional vector spaces. The notions of linear dependence and independence, as well as linear combinations, and hence the notion of basis will be presented. Some results about the dimension of the different basis of a vector space will be necessary, as well as on the isomorphism among vector spaces. Once we have introduced the notion of basis, and with the additional condition of it being finite, we will introduce the notion of finite-dimensional vector space. Next step is to introduce vector subspaces. We will pay attention to vector susbpaces generated by a given set of vectors and prove some of their properties. The notion of linear maps will be also required to define isomorphisms of vector spaces. Finally, we will prove that a vector space (over a field
.
The previous results will be presented following the book by Halmos on vector spaces [1]. Its formalization will be carried out in Isabelle/HOL.
El código de la formalización se encuentra aquí.
Una extensión del trabajo es Formalizing an abstract algebra textbook in Isabelle/HOL presentado el 14 de junio de 2012 en el EACA 2012 (EACA 2012
XIII Encuentro de Álgebra Computacional y Aplicaciones).
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.