{"id":3430,"date":"2013-07-03T04:04:35","date_gmt":"2013-07-03T04:04:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3430"},"modified":"2013-07-03T04:06:05","modified_gmt":"2013-07-03T04:06:05","slug":"resena-formalizing-cut-elimination-of-coalgebraic-logics-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalizing-cut-elimination-of-coalgebraic-logics-in-coq\/","title":{"rendered":"Rese\u00f1a: &#8220;Formalizing cut elimination of coalgebraic logics in Coq&#8221;"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre metal\u00f3gica titulado <a href=\"http:\/\/askra.de\/papers\/cut-eli.pdf\">Formalizing cut elimination of coalgebraic logics in Coq<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/askra.de\/index.html.en\">Hendrik Tews<\/a> (de la <i>Dresden University of Technology<\/i>) y se presentar\u00e1 en el <a href=\"http:\/\/tableaux13.loria.fr\">Tableaux 2013<\/a> (<i>Automated Reasoning with Analytic Tableaux and Related Methods<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nIn their <a href=\"http:\/\/www.doc.ic.ac.uk\/~dirk\/Publications\/ic2010.pdf\">work on coalgebraic logics<\/a>, Pattinson and Schr\u00f6der prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics. The present paper reports on a formalization of Pattinson\u2019s and Schr\u00f6der\u2019s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/askra.de\/science\/coalgebraic-cut\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre metal\u00f3gica titulado Formalizing cut elimination of coalgebraic logics in Coq. Su autor es Hendrik Tews (de la Dresden University of Technology) y se presentar\u00e1 en el Tableaux 2013 (Automated Reasoning with Analytic Tableaux and Related Methods). Su resumen es In their work on coalgebraic&#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,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\/3430"}],"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=3430"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3430\/revisions"}],"predecessor-version":[{"id":3432,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3430\/revisions\/3432"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3430"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3430"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3430"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}