Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422138 | Electronic Notes in Theoretical Computer Science | 2008 | 14 Pages |
Abstract
This paper takes first steps towards a formalization of graph transformations in a general setting of interactive theorem provers, which will form the basis for proofs of correctness of graph transformation systems. Whereas graph rewriting is usually performed by mapping a pattern graph into a source graph by means of a graph morphism and then carrying out operations on the image node and edge set, this article generalises the notion of pattern graph to path expressions, which are formulae in a fragment of first-order logic. We examine the correspondence with traditional graph rewriting and show that this interpretation is beneficial when formally reasoning about model transformations with the aid of proof assistants.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics