Algebraic Graph Derivations for Graphical Calculi

Wolfram Kahl

pp . 224-238 in Fabrizio d'Amore, Paola G. Franciosa, Alberto Marchetti-Spaccamela (eds): Graph Theoretic Concepts in Computer Science, 22nd International Workshop, WG '96, Caddenabbia, Italy, June 1996, Proceedings, LNCS 1197, Springer-Verlag 1997

(.bib, .ps.gz, .pdf)

Introduction

Relational formalisations can be very concise and precise and can allow short, calculational proofs under certain circumstances. [...] In situations corresponding to the simultaneous use of many variables in predicate logic, however, either a style using predicate logic with point variables has to be adopted or impractical and clumsy manipulations of tuples have to be employed inside relation calculus. In the application of relational formalisation to term graphs with bound variables [...] we have been forced to employ both methods extensively, and, independently of other approaches, have been driven to develop a graphical calculus for making complex relation algebraic proofs more accessible.

It turns out that, although our approach shares many common points with those presented in the literature [...], it still is more general and more flexible than those approaches since we draw heavily on additional background in algebraic graph rewriting

Contents

• Introduction
• Type and Relation Terms
• Relational Diagrams
  • Syntax
  • Semantics
  • Examples without Hyperedges
  • Example with Hyperedges
• Extension to Branching Derivations
• Outlook and Conclusion

This work is continued in [Kahl-1999d].