Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem

DOI10.1007/978-3-031-36709-0_7zbMath1545.68065MaRDI QIDQ6535510

Unnamed Author, Detlef Plump

Publication date: 12 January 2024

zbMATH Keywords

Isabelle/HOLChurch-Rosser theoremdouble-pushout graph transformationuniqueness of derivations

Mathematics Subject Classification ID

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

Related Items (1)

Formalising the double-pushout approach to graph transformation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elements of finite model theory.
• Deriving graphs from graphs by applying a production
• A graph library for Isabelle
• Verifying graph programs with monadic second-order logic
• From LCF to Isabelle/HOL
• Theorem proving graph grammars with attributes and negative application conditions
• Fundamentals of algebraic graph transformation
• Double-pushout graph transformation revisited
• Concrete Semantics
• The Four Colour Theorem: Engineering of a Formal Proof
• Pushout-Properties: An analysis of gluing constructions for graphs
• Interactive and automated proofs for graph transformations
• Logic in Computer Science
• A formally verified proof of the prime number theorem
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Foundations of Software Science and Computation Structures

This page was built for publication: Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem