{"id":3475,"date":"2013-08-07T23:55:31","date_gmt":"2013-08-07T23:55:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3475"},"modified":"2013-08-07T15:21:17","modified_gmt":"2013-08-07T15:21:17","slug":"formalization-of-basic-linear-algebra","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formalization-of-basic-linear-algebra\/","title":{"rendered":"Formalization of basic linear algebra"},"content":{"rendered":"<p>Se ha publicado una tesis de m\u00e1ster de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> titulada <a href=\"http:\/\/scholarworks.csusm.edu\/bitstream\/handle\/10211.8\/405\/TalsaniaBhavisha_Spring2013.pdf?sequence=1\">Formalization of basic linear algebra<\/a>.<\/p>\n<p>Su autor es Bhavisha M. Talsania (de la <i>California State University, San Marcos<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis thesis discusses the formalization of basic results from linear algebra up to the following theorems, using the computer proof checker Isabelle:<\/p>\n<ul>\n<li>Theorem 1 (Basis Size Theorem): Suppose that V is a finite dimensional vector space. Then any two bases have the same number of elements.\n<li>Theorem 2 (Basis Characterization Theorem): Suppose that V is a vector space of dimension n. Then any spanning set has at least n elements, and any spanning set with exactly n elements is a basis. In addition, any linearly independent set of vectors has at most n elements, and any set of linearly independent vectors with exactly n elements is a basis.\n<li>Theorem 3 (Rank-Nullity Theorem): Let L : V1 \u2192 V2 be a linear map between finite dimensional vector spaces. Then the nullity of L plus the rank of L equals the dimension of V1 : dim(V1 ) = rank(L) + null(L).\n<\/ul>\n<p>Chapter 1 provides a discussion of informal and formal proofs and an introduction to the thesis topic. Chapter 2 provides a brief overview of the proof assistant Isabelle and it\u2019s layout and syntax. Chapter 3 to Chapter 13 go into detail of the formalized proofs done in Isabelle. In Chapter 14, we end with remarks and conclusion of the thesis.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado una tesis de m\u00e1ster de razonamiento formalizado en Isabelle\/HOL titulada Formalization of basic linear algebra. Su autor es Bhavisha M. Talsania (de la California State University, San Marcos). Su resumen es This thesis discusses the formalization of basic results from linear algebra up to the following theorems, using the computer proof checker&#8230;<\/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":[1],"tags":[144,37],"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\/3475"}],"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=3475"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3475\/revisions"}],"predecessor-version":[{"id":3476,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3475\/revisions\/3476"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3475"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3475"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3475"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}