{"id":6204,"date":"2018-09-05T18:43:15","date_gmt":"2018-09-05T16:43:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6204"},"modified":"2018-09-05T18:44:25","modified_gmt":"2018-09-05T16:44:25","slug":"resena-a-formal-proof-of-the-computation-of-hermite-normal-form-in-a-general-setting","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-formal-proof-of-the-computation-of-hermite-normal-form-in-a-general-setting\/","title":{"rendered":"Rese\u00f1a: A formal proof of the computation of Hermite normal form in a general setting"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00e1lgebra lineal titulado <a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\/publications\/2018\/AISC_2018.pdf\">REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\">Jose Divas\u00f3n<\/a> y <a href=\"http:\/\/www.unirioja.es\/cu\/jearansa\">Jes\u00fas Aransay<\/a> (de la Universidad de la Rioja).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>In this work, we present a formal proof of an algorithm to compute the Hermite normal form of a matrix based on our existing framework for the formalisation, execution, and refinement of linear algebra algorithms in Isabelle\/HOL. The Hermite normal form is a well-known canonical matrix analogue of reduced echelon form of matrices over fields, but involving matrices over more general rings, such as Be\u0301zout domains. We prove the correctness of this algorithm and formalise the uniqueness of the Hermite normal form of a matrix. The succinctness and clarity of the formalisation validate the usability of the framework.<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el 17 de septiembre en el <a href=\"http:\/\/aisc2018.cc4cm.org\/\">AISC 2018<\/a> (<i>13th International Conference on Artificial Intelligence and Symbolic Computation<\/i>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\/Isabelle\/Hermite\/Hermite.html\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00e1lgebra lineal titulado REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting. Sus autores son Jose Divas\u00f3n y Jes\u00fas Aransay (de la Universidad de la Rioja). Su resumen es In this work, we present a formal proof of&#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":[100],"tags":[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\/6204"}],"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=6204"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6204\/revisions"}],"predecessor-version":[{"id":6206,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6204\/revisions\/6206"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6204"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6204"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6204"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}