Interactive and automated proofs for graph transformations

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.
 

Online Copy

PDF (author's copy)

Isabelle development

BibTeX Entry

@Article{strecker18:_proofs_graph_trans,
  author =       {Martin Strecker},
  title =        {Interactive and automated proofs for graph transformations},
  journal =      {Mathematical Structures in Computer Science},
  volume    = 28,
  number    = 8,
  pages     = {1333--1362},
  year =         2018,
  url       = {https://www.irit.fr/~Martin.Strecker/Publications/proofs_graph_transformations.html}
}