{"id":3477,"date":"2013-08-09T06:31:28","date_gmt":"2013-08-09T06:31:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3477"},"modified":"2013-08-09T06:34:13","modified_gmt":"2013-08-09T06:34:13","slug":"verifying-the-bridge-between-simplicial-topology-and-algebra-the-eilenberg-zilber-algorithm","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/verifying-the-bridge-between-simplicial-topology-and-algebra-the-eilenberg-zilber-algorithm\/","title":{"rendered":"Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm"},"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:\/\/wiki.portal.chalmers.se\/cse\/uploads\/ForMath\/vbbstaeza\">Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"https:\/\/esus.unirioja.es\/psycotrip\/index.php?op=miembro&#038;miembro=0005\">Laureano Lamb\u00e1n<\/a> (de la Universidad de la Rioja),\n<li><a href=\"<a href=\"https:\/\/esus.unirioja.es\/psycotrip\/index.php?op=miembro&#038;miembro=0001\">Julio Rubio<\/a> (de la Universidad de la Rioja),\n<li><a href=\"https:\/\/www.glc.us.es\/fmartin\/\">Francisco J. Mart\u00edn Mateos<\/a> (de la Universidad de Sevilla) y\n<li><a href=\"http:\/\/www.cs.us.es\/~jruiz\/\">Jos\u00e9 L. Ruiz Reina<\/a> (de la Universidad de Sevilla).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe Eilenberg\u2013Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted to computing in Algebraic Topology. In this article we report on a complete formal proof of the underlying Eilenberg\u2013Zilber theorem, using the ACL2 theorem prover. As our formalization is executable, we are able to compare the results of the certified programme with those of Kenzo on some universal examples. Since the results coincide, the reliability of Kenzo is reinforced. This is a new step in our long-term project towards certified programming for Algebraic Topology.\n<\/p><\/blockquote>\n<p>El art\u00edculo se ha publicado en <a href=\"http:\/\/jigpal.oxfordjournals.org\/content\/early\/2013\/08\/06\/jigpal.jzt034.short?rss=1\">Logic Journal of the IGPL<\/a>.<\/p>\n<p>Los c\u00f3digos de las correspondientes teor\u00edas en ACL2 se encuentran <a href=\"https:\/\/www.glc.us.es\/ITP2011\/index.php?option=com_content&#038;view=article&#038;id=3:overview\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en ACL2 titulado Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. Sus autores son Laureano Lamb\u00e1n (de la Universidad de la Rioja),<\/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,273,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\/3477"}],"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=3477"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3477\/revisions"}],"predecessor-version":[{"id":3481,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3477\/revisions\/3481"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3477"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3477"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3477"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}