Formalising the double-pushout approach to graph transformation

DOI10.46298/LMCS-20(4:3)2024MaRDI QIDQ6635513zbMATH OpenFDO

Authors Detlef Plump

Publication date 12 November 2024

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-20(4:3)2024

zbMATH Keywords

Church-Rosser theoremdouble-pushout graph transformationIsabelle/HOLuniqueness of derivations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formalization of linear space theory in the higher-order logic proving system
• Towards mechanised proofs in double-pushout graph transformation
• Category theory in Isabelle/HOL as a basis for meta-logical investigation
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• Formalizing Hilbert's Grundlagen in Isabelle/Isar

Cites work

• A formal proof of the Kepler conjecture
• A formally verified proof of the prime number theorem
• A graph library for Isabelle
• Concrete semantics. With Isabelle/HOL
• Deriving graphs from graphs by applying a production
• Double-pushout graph transformation revisited
• Elements of finite model theory.
• Formalising the double-pushout approach to graph transformation
• Foundations of Software Science and Computation Structures
• From LCF to Isabelle/HOL
• Fundamentals of algebraic graph transformation
• scientific article; zbMATH DE number 3548465 (Why is no real title available?)
• scientific article; zbMATH DE number 7015112 (Why is no real title available?)
• Interactive and automated proofs for graph transformations
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Logic in Computer Science
• Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
• Proceedings of the Thirteenth International Workshop on Graph Computation Models
• Pushout-Properties: An analysis of gluing constructions for graphs
• Reasoning about graph programs
• The Four Colour Theorem: Engineering of a Formal Proof
• Theorem proving graph grammars with attributes and negative application conditions
• Verifying graph programs with monadic second-order logic

Cited in

(2)

• Re-imagining the Isabelle archive of formal proofs
• Formalising the double-pushout approach to graph transformation

This page was built for publication: Formalising the double-pushout approach to graph transformation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6635513)