{"id":5475,"date":"2016-08-11T12:22:56","date_gmt":"2016-08-11T10:22:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5475"},"modified":"2016-08-11T12:22:56","modified_gmt":"2016-08-11T10:22:56","slug":"resena-relation-algebraic-verification-of-prims-minimum-spanning-tree-algorithm","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-relation-algebraic-verification-of-prims-minimum-spanning-tree-algorithm\/","title":{"rendered":"Rese\u00f1a: Relation-algebraic verification of Prim\u2019s minimum spanning tree algorithm"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado <a href=\"http:\/\/www.csse.canterbury.ac.nz\/walter.guttmann\/publications\/0048.pdf\">Relation-algebraic verification of Prim\u2019s minimum spanning tree algorithm<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.csse.canterbury.ac.nz\/walter.guttmann\">Walter Guttmann<\/a> (de la <em>University of Canterbury<\/em>, Nueva Zelanda).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We formally prove the correctness of Prim&#8217;s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle\/HOL heavily using its integrated automated theorem provers.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el 24 de octubre en el <a href=\"http:\/\/cc.ee.ntu.edu.tw\/~ictac2016\/\">ICTAC2016<\/a> (<em>13th International Colloquium on Theoretical Aspects of Computing<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/www.csse.canterbury.ac.nz\/walter.guttmann\/algebra\/isabelle\/MST.zip\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Relation-algebraic verification of Prim\u2019s minimum spanning tree algorithm. Su autor es Walter Guttmann (de la University of Canterbury, Nueva Zelanda). Su resumen es We formally prove the correctness of Prim&#8217;s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and&#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\/5475"}],"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=5475"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5475\/revisions"}],"predecessor-version":[{"id":5476,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5475\/revisions\/5476"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5475"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5475"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5475"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}