Spider Graphs: a graph transformation system for spider diagrams

Paolo Bottoni, Andrew Fish, Francesco Parisi-Presicce

Research output: Contribution to journalArticle

Abstract

The use of diagrammatic logic as a reasoning mechanism to produce inferences on subsets of some universe could provide a way to overcome the current limitations of visual modelling methods, which have to be integrated with textual languages to express complex constraints. On the other hand, graph transformations are becoming widespread as a way to express formal semantics for visual modelling languages, so that a mechanisation of diagrammatic logic based on graph transformation would facilitate language integration, based on a common underlying machinery. In this paper, we propose such a mechanisation for spider diagrams (SDs), an established language for reasoning with diagrams modelling relations between sets and constraints on their cardinalities. The concrete syntax of SDs extends that of Euler diagrams that use closed curves and the enclosed regions to represent sets and their intersections. The language is augmented with reasoning rules, i.e. syntactic transformation rules corresponding to logical inference rules. However, these rules are typically defined in procedural terms, so that a completely formal specification and an adequate mechanisation of them has not been achieved yet. We propose an abstract syntax for SDs in terms of typed graphs and define the corresponding language of Spider Graphs (SGs), expressing reasoning rules for SDs as graph transformation units. This enables a direct realisation of the reasoning system via graph transformation tools without resorting to ad hoc implementations, and we provide an implementation in AGG. Techniques for static analysis become available to reason on proof strategies and on possible optimisations.
Original languageEnglish
Pages (from-to)1421-1453
Number of pages33
JournalSoftware and Systems Modeling
Volume14
Issue number4
DOIs
Publication statusPublished - 1 Oct 2015

Bibliographical note

The final publication is available at Springer via http://dx.doi.org/10.1007/s10270-013-0381-1

Fingerprint Dive into the research topics of 'Spider Graphs: a graph transformation system for spider diagrams'. Together they form a unique fingerprint.

  • Cite this