{"id":4968,"date":"2015-08-14T19:08:25","date_gmt":"2015-08-14T17:08:25","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4968"},"modified":"2015-08-14T19:08:25","modified_gmt":"2015-08-14T17:08:25","slug":"resena-a-symbolic-approach-to-abstract-algebra-in-hol-light","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-symbolic-approach-to-abstract-algebra-in-hol-light\/","title":{"rendered":"Rese\u00f1a: A symbolic approach to abstract algebra in HOL Light"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\">HOL Light<\/a> sobre \u00e1lgebra titulado <a href=\"http:\/\/www.cicm-conference.org\/2015\/fm4m\/FMM_2015_paper_1.pdf\">A symbolic approach to abstract algebra in HOL Light<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.math.unifi.it\/~maggesi\">Marco Maggesi<\/a> (de la Univ. de Florencia en Italia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, &#8230;) is known to be challenging task which is often undertaken by exploiting various kind of extra-logical mechanisms (axiomatic classes, modules, locales, coercions, &#8230;) provided by most modern theorem provers.<\/p>\n<p>  We want to explore an alternative strategy, where algebraic structures are implemented via a deep embedding of mathematical formulas and are managed as first class objects in the HOL theory. Along the way, we provide a mechanism of <em>generalised conversions<\/em>, which extends Paulson\u2019s conversions by allowing to compute with equivalence relations. We developed generalised conversions to support rewriting in our system, but they can be used independently and may have an interest in its own.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en <a href=\"http:\/\/bit.ly\/1PcLm0B\">CICM 2015<\/a> (<em>the 8th Conference on Intelligent Computer Mathematics<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en HOL Light se encuentra <a href=\"https:\/\/bitbucket.org\/maggesi\/symbolic\/src\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en HOL Light sobre \u00e1lgebra titulado A symbolic approach to abstract algebra in HOL Light. Su autor es Marco Maggesi (de la Univ. de Florencia en Italia). Su resumen es Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, &#8230;) is known to be challenging task which&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[22,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\/4968"}],"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=4968"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4968\/revisions"}],"predecessor-version":[{"id":4969,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4968\/revisions\/4969"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4968"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4968"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4968"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}