{"id":3235,"date":"2013-04-16T05:39:47","date_gmt":"2013-04-16T05:39:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3235"},"modified":"2013-04-16T05:40:35","modified_gmt":"2013-04-16T05:40:35","slug":"resena-coinductive-pearl-modular-first-order-logic-completeness","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-coinductive-pearl-modular-first-order-logic-completeness\/","title":{"rendered":"Rese\u00f1a: Coinductive pearl: Modular first-order logic completeness"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre metal\u00f3gica titulado <a href=\"http:\/\/home.in.tum.de\/~traytel\/papers\/fol_completeness\/compl.pdf\">Coinductive pearl: Modular first-order logic completeness<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www21.in.tum.de\/~blanchet\">Jasmin Christian Blanchette<\/a>, <a href=\"http:\/\/www21.in.tum.de\/~popescua\/\">Andrei Popescu<\/a> y <a href=\"http:\/\/home.in.tum.de\/~traytel\/\">Dmitriy Traytel<\/a> (de la Universidad T\u00e9cnica de Munich).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nCodatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the <a href=\"http:\/\/en.wikipedia.org\/wiki\/G%C3%B6del%27s_completeness_theorem\">completeness theorem for first-order logic<\/a> established through a <a href=\"http:\/\/planetmath.org\/gentzensystem\">Gentzen system<\/a>. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> and demonstrates the <a href=\"http:\/\/www21.in.tum.de\/~blanchet\/lics2012-codat.pdf\">recently introduced definitional package for codatatypes<\/a> and its integration with Isabelle&#8217;s Haskell code generator.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las teor\u00edas Isabelle correspodientes se encuentra <a href=\"http:\/\/www21.in.tum.de\/~popescua\/compl_devel.zip\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre metal\u00f3gica titulado Coinductive pearl: Modular first-order logic completeness. Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad T\u00e9cnica de Munich). Su resumen es Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case&#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":[270,144,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\/3235"}],"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=3235"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3235\/revisions"}],"predecessor-version":[{"id":3237,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3235\/revisions\/3237"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3235"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3235"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3235"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}