Reseña: Interactive and automated proofs for graph transformations
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, 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.
El código de la formalización se encuentra aquí.