{"id":7067,"date":"2020-03-01T10:56:23","date_gmt":"2020-03-01T09:56:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7067"},"modified":"2020-03-01T10:56:23","modified_gmt":"2020-03-01T09:56:23","slug":"resena-graph-theory-in-coq-minors-treewidth-and-isomorphisms","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-graph-theory-in-coq-minors-treewidth-and-isomorphisms\/","title":{"rendered":"Rese\u00f1a: Graph theory in Coq: minors, treewidth, and isomorphisms"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq\/Ssreflect sobre grafos titulado <a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02316859v2\/document\">Graph theory in Coq: minors, treewidth, and isomorphisms<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/perso.ens-lyon.fr\/christian.doczkal\/\">Christian Doczkal<\/a> (Universite\u0301 Co\u0302te d\u2019Azur, Inria Sopia Antipolis Me\u0301diterrane\u0301e, France) y<\/li>\n<li><a href=\"http:\/\/perso.ens-lyon.fr\/damien.pous\/\">Damien Pous<\/a> (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>We present a library for graph theory in Coq\/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger&#8217;s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.<\/p><\/blockquote>\n<p>El trabajo se ha publicado en el <a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09543-2\">Journal of Automated Reasoning<\/a><\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"https:\/\/perso.ens-lyon.fr\/damien.pous\/covece\/graphs\/\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq\/Ssreflect sobre grafos titulado Graph theory in Coq: minors, treewidth, and isomorphisms. Sus autores son Christian Doczkal (Universite\u0301 Co\u0302te d\u2019Azur, Inria Sopia Antipolis Me\u0301diterrane\u0301e, France) y Damien Pous (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France). Su resumen es We present a library&#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":[100],"tags":[],"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\/7067"}],"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=7067"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7067\/revisions"}],"predecessor-version":[{"id":7068,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7067\/revisions\/7068"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7067"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7067"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7067"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}