Towards a Formalisation of Graph Transformations in Proof Assistants

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. We present parts of our formalization and take a glimpse at some strategies for simplifying proof obligations.
 

Online Copy

Available as PDF
 

BibTeX Entry

@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}}
}