Formalising the Double-Pushout Approach to Graph Transformation
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916439163666432 |
|---|---|
| author | Söldner, Robert Plump, Detlef |
| author_facet | Söldner, Robert Plump, Detlef |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_15641 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Formalising the Double-Pushout Approach to Graph Transformation Söldner, Robert Plump, Detlef Logic in Computer Science 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. |
| title | Formalising the Double-Pushout Approach to Graph Transformation |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2312.15641 |