{"id":2159,"date":"2012-09-02T05:26:40","date_gmt":"2012-09-02T05:26:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2159"},"modified":"2013-03-08T05:48:12","modified_gmt":"2013-03-08T05:48:12","slug":"interactive-and-automated-proofs-for-graph-transformations","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/interactive-and-automated-proofs-for-graph-transformations\/","title":{"rendered":"Rese\u00f1a: Interactive and automated proofs for graph transformations"},"content":{"rendered":"<p>Se ha publicado un trabajo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/www.irit.fr\/~Martin.Strecker\/Publications\/proofs_graph_transformations.pdf\">Interactive and automated proofs for graph transformations<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.irit.fr\/~Martin.Strecker\">Martin Strecker<\/a> (de la <i>Univ. Paul Sabatier<\/i>, Toulouse, Francia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de la formalizaci\u00f3n se encuentra <a href=\"http:\/\/www.irit.fr\/~Martin.Strecker\/Publications\/proofs_graph_transformations.tgz\">aqu\u00ed<\/a>.  <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un trabajo de razonamiento formalizado en Isabelle\/HOL titulado Interactive and automated proofs for graph transformations. Su autor es Martin Strecker (de la Univ. Paul Sabatier, Toulouse, Francia). Su resumen es This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs,&#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":[89,144,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\/2159"}],"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=2159"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2159\/revisions"}],"predecessor-version":[{"id":2783,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2159\/revisions\/2783"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2159"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2159"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2159"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}