Proof Tactics for Theorem Proving Graph Grammars through Rodin

Graph grammar is a formal language suitable for the specification of distributed and concurrent systems. Theorem proving is a technique that allows the verification of systems with huge (and infinite) state space. One of the disadvantages of theorem proving graph grammars (and theorem proving in general) is the specific mathematical knowledge required from the user for concluding the proofs. Previous works have proposed proof strategies to help the developer in the verification process when adopting such approach, firstly establishing proof tactics for some properties and after proposing a visual representation for them. This paper extends the set of proposed tactics, with the aim of expanding the available strategies and encouraging the use of such a technique