Towards a Formalisation of Graph Transformations in Proof Assistants

Martin Strecker (1) , Mathieu Giorgino (1)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées

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.

Mots clés: Theorem Proving; Graph Transformations

Domaines: Logique en informatique [cs.LO]

Martin Strecker, Mathieu Giorgino. Towards a Formalisation of Graph Transformations in Proof Assistants. Automatic Verification of Critical Systems, Sep 2006, Nancy, France. pp.178-183. ⟨inria-00091666⟩