{"id":3376,"date":"2013-05-28T04:44:49","date_gmt":"2013-05-28T04:44:49","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3376"},"modified":"2013-05-28T04:45:37","modified_gmt":"2013-05-28T04:45:37","slug":"resena-the-rooster-and-the-butterflies-a-machine-checked-proof-of-the-jordan-holder-theorem-for-finite-groups","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-the-rooster-and-the-butterflies-a-machine-checked-proof-of-the-jordan-holder-theorem-for-finite-groups\/","title":{"rendered":"Rese\u00f1a: The rooster and the butterflies (a machine-checked proof of the Jordan-H\u00f6lder theorem for finite groups)"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre la demostraci\u00f3n del teorema de Jordan-H\u00f6lder para grupos finitos titulado <a href=\"http:\/\/hal.inria.fr\/docs\/00\/82\/50\/74\/PDF\/main.pdf\">The rooster and the butterflies<\/a>.<\/p>\n<p>Su autora es <a href=\"http:\/\/specfun.inria.fr\/mahboubi\/\">Assia Mahboubi<\/a> (de <i>Microsoft Research &#8211; Inria Joint Centre<\/i>).<\/p>\n<p>El trabajo se presentar\u00e1 en julio en el <a href=\"http:\/\/www.cicm-conference.org\/2013\/cicm.php\">CICM 2013<\/a> (<i>Conferences on Intelligent Computer Mathematics<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis paper describes a machine-checked proof of the <a href=\"http:\/\/mathworld.wolfram.com\/Jordan-HoelderTheorem.html\">Jordan-H\u00f6lder theorem<\/a> for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre la demostraci\u00f3n del teorema de Jordan-H\u00f6lder para grupos finitos titulado The rooster and the butterflies. Su autora es Assia Mahboubi (de Microsoft Research &#8211; Inria Joint Centre). El trabajo se presentar\u00e1 en julio en el CICM 2013 (Conferences on Intelligent Computer Mathematics). Su resumen&#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":[45,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\/3376"}],"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=3376"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3376\/revisions"}],"predecessor-version":[{"id":3378,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3376\/revisions\/3378"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3376"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3376"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3376"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}