English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In this paper, we utilize Isabelle/HOL to develop a formal framework for thebasic theory of double-pushout graph transformation. Our work includes definingessential concepts like graphs, morphisms, pushouts, and pullbacks, anddemonstrating their properties. We establish the uniqueness of derivations,drawing upon Rosens 1975 research, and verify the Church-Rosser theorem usingEhrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of ourformalisation approach. The paper details our methodology in employingIsabelle/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 ofworking with an Interactive Theorem Prover. This work emphasizes the increasingimportance of formal verification tools in clarifying complex mathematicalconcepts.

Formalising the Double-Pushout Approach to Graph Transformation