This paper takes first steps towards a formalisation of graph transformations in a general setting of interactive theorem provers, which will form the basis for proofs of correctness of graph transformation systems. We present parts of our formalisation and take a glimpse at some strategies for simplifying proof obligations.
(preliminary)
@InProceedings{strecker06:_towar_formal_graph_trans_proof_assis,
author = {Martin Strecker and Mathieu Giorgino},
title = {Towards a Formalisation of Graph Transformations in Proof Assistants},
booktitle = {Proc. AVOCS'06},
year = 2006,
month = sep,
note = {\url{http://www.irit.fr/~Martin.Strecker/Publications/avocs06.html}}
}