Showing 1–2 of 2 results for author: Söldner, R

Formalising the Double-Pushout Approach to Graph Transformation

Authors: Robert Söldner, Detlef Plump

Abstract: In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreows… ▽ More In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our formalisation approach. The paper details our methodology in employing Isabelle/HOL, including key design decisions that shaped the current iteration. We explore the technical complexities involved in applying higher-order logic, aiming to give readers an insightful perspective into the engaging aspects of working with an Interactive Theorem Prover. This work emphasizes the increasing importance of formal verification tools in clarifying complex mathematical concepts. △ Less

Submitted 5 October, 2024; v1 submitted 25 December, 2023; originally announced December 2023.

Journal ref: Logical Methods in Computer Science, Volume 20, Issue 4 (October 4, 2024) lmcs:12748

Towards Mechanised Proofs in Double-Pushout Graph Transformation

Authors: Robert Söldner, Detlef Plump

Abstract: We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition of direct derivations based on deletion and gluing. We then formalise graph pushouts and prove with Isabelle's help that both deletions and gluings are pushout… ▽ More We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition of direct derivations based on deletion and gluing. We then formalise graph pushouts and prove with Isabelle's help that both deletions and gluings are pushouts. We also prove that pushouts are unique up to isomorphism. The formalisation comprises around 2000 lines of source text. Our motivation is to pave the way for rigorous, machine-checked proofs in the theory of the double-pushout approach, and to lay the foundations for verifying graph transformation systems and rule-based graph programs by interactive theorem proving. △ Less

Submitted 22 December, 2022; originally announced December 2022.

Comments: In Proceedings GCM 2022, arXiv:2212.10975

ACM Class: F.4.1; F.4.2; G.2.2

Journal ref: EPTCS 374, 2022, pp. 59-75