{"id":3134,"date":"2013-03-21T05:31:34","date_gmt":"2013-03-21T05:31:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3134"},"modified":"2013-03-21T05:32:11","modified_gmt":"2013-03-21T05:32:11","slug":"resena-a-hierarchy-of-mathematical-structures-in-acl2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-hierarchy-of-mathematical-structures-in-acl2\/","title":{"rendered":"Rese\u00f1a: A hierarchy of mathematical structures in ACL2"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cs.utexas.edu\/~moore\/acl2\">ACL2<\/a> titulado <a href=\"http:\/\/www.computing.dundee.ac.uk\/staff\/jheras\/papers\/ahomsia.pdf\">A hierarchy of mathematical structures in ACL2<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.computing.dundee.ac.uk\/staff\/jheras\">J\u00f3nathan Heras<\/a>, <a href=\"https:\/\/www.glc.us.es\/fmartin\">Francisco J. Mart\u00edn<\/a> y <a href=\"http:\/\/www.unirioja.es\/cu\/mvico\">Vico Pascual<\/a>.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nIn this paper, we present a methodology which allows one to deal with mathematical structures in the ACL2 theorem prover. Namely, we cope with the representation of mathematical structures, the certification that an object fulfills the axioms characterizing an algebraic structure and the generation of generic theories about concrete structures. As a by-product, an ACL2 algebraic hierarchy has been obtained. Our framework has been tested with the definition of homology groups, an example coming from Homological Algebra which involves several notions related to Universal Algebra. The method presented here, when compared to a from-scratch approach, is preferred when working with complex mathematical structures; for instance, the ones coming from Algebraic Topology. The final aim of this work is the verification of Computer Algebra systems, a field where our hierarchy fits better than the ones developed in other systems.  <\/p><\/blockquote>\n<p>El c\u00f3dico correspondiente a este trabajo se encuentra <a href=\"http:\/\/www.computing.dundee.ac.uk\/staff\/jheras\/ahomsia\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en ACL2 titulado A hierarchy of mathematical structures in ACL2. Sus autores son J\u00f3nathan Heras, Francisco J. Mart\u00edn y Vico Pascual. Su resumen es In this paper, we present a methodology which allows one to deal with mathematical structures in the ACL2 theorem prover. Namely, we cope&#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":[49,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\/3134"}],"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=3134"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3134\/revisions"}],"predecessor-version":[{"id":3136,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3134\/revisions\/3136"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3134"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3134"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3134"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}