{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T01:31:59Z","timestamp":1772069519458,"version":"3.50.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In this paper, we utilize Isabelle\/HOL to develop a formal framework for the\nbasic theory of double-pushout graph transformation. Our work includes defining\nessential concepts like graphs, morphisms, pushouts, and pullbacks, and\ndemonstrating their properties. We establish the uniqueness of derivations,\ndrawing upon Rosens 1975 research, and verify the Church-Rosser theorem using\nEhrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our\nformalisation approach. The paper details our methodology in employing\nIsabelle\/HOL, including key design decisions that shaped the current iteration.\nWe explore the technical complexities involved in applying higher-order logic,\naiming to give readers an insightful perspective into the engaging aspects of\nworking with an Interactive Theorem Prover. This work emphasizes the increasing\nimportance of formal verification tools in clarifying complex mathematical\nconcepts.<\/jats:p>","DOI":"10.46298\/lmcs-20(4:3)2024","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T17:20:08Z","timestamp":1728408008000},"source":"Crossref","is-referenced-by-count":2,"title":["Formalising the Double-Pushout Approach to Graph Transformation"],"prefix":"10.46298","volume":"Volume 20, Issue 4","author":[{"given":"Robert","family":"S\u00f6ldner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Detlef","family":"Plump","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2024,10,8]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/14420\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/14420\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T17:20:08Z","timestamp":1728408008000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/12748"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(4:3)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2312.15641v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2312.15641v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2312.15641","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2312.15641","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"article-number":"12748"}}