{"id":2138,"date":"2012-08-20T01:39:15","date_gmt":"2012-08-20T01:39:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2138"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"proofs-of-properties-of-finite-dimensional-vector-spaces-using-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/proofs-of-properties-of-finite-dimensional-vector-spaces-using-isabellehol\/","title":{"rendered":"Rese\u00f1a: Proofs of properties of finite-dimensional vector spaces using Isabelle\/HOL"},"content":{"rendered":"

Se ha publicado un trabajo de razonamiento formalizado en Isabelle\/HOL<\/a>, titulada Proofs of properties of finite-dimensional vector spaces using Isabelle\/HOL<\/a>.<\/p>\n

Su autor es Jose Divas\u00f3n Mallagaray, dirigido por Jes\u00fas Mar\u00eda Aransay Azofra<\/a> (de la Univ. de la Rioja).<\/p>\n

La presentaci\u00f3n<\/a> del trabajo tuvo lugar el 25 de Octubre de 2011 en la Universidad de la Rioja.<\/p>\n

El objetivo del trabajo es la formalizaci\u00f3n en Isabelle\/HOL de conceptos y teoremas sobre \u00e1lgebra lineal siguiendo la 16 primeras secciones del libro de Halmos Finite-dimensional vector spaces<\/a>. <\/p>\n

El resumen del trabajo es<\/p>\n

\nIn this work we deal with finite-dimensional vector spaces over a generic field \"\mathbb{K}\". 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 \"\mathbb{K}\") of (finite) dimension n is isomorphic to \"\mathbb{K}^n\". <\/p>\n

The previous results will be presented following the book by Halmos on vector spaces [1]<\/a>. Its formalization will be carried out in Isabelle\/HOL<\/a>.\n<\/p><\/blockquote>\n

El c\u00f3digo de la formalizaci\u00f3n se encuentra aqu\u00ed<\/a>. <\/p>\n

Una extensi\u00f3n del trabajo es Formalizing an abstract algebra textbook in Isabelle\/HOL<\/a> presentado el 14 de junio de 2012 en el EACA 2012<\/a> (EACA 2012
\nXIII Encuentro de \u00c1lgebra Computacional y Aplicaciones). <\/p>\n

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

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\u00f3n Mallagaray, dirigido por Jes\u00fas Mar\u00eda Aransay Azofra (de la Univ. de la Rioja). La presentaci\u00f3n del trabajo tuvo lugar el 25 de Octubre de 2011 en la Universidad de la…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[89,144,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2138"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=2138"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2138\/revisions"}],"predecessor-version":[{"id":2791,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2138\/revisions\/2791"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2138"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2138"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2138"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}