Rewriting with generalized nominal unification

DOI10.1017/S0960129520000122zbMath1495.68115OpenAlexW3027318171MaRDI QIDQ5139280

Yunus D. K. Kutz, Manfred Schmidt-Schauss

Publication date: 8 December 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129520000122

zbMATH Keywords

confluencenominal unificationatom-variablesnominal rewritingKnuth-Bendix confluence criterion

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Grammars and rewriting systems (68Q42)

Related Items

Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting ⋮ Confluence and commutation for nominal rewriting systems with atom-variables ⋮ Nominal unification with letrec and environment-variables

Uses Software

• Haskell
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equivariant unification
• Nominal techniques in Isabelle/HOL
• A polynomial nominal unification algorithm
• Nominal unification with atom-variables
• Parallel closure theorem for left-linear nominal rewriting systems
• Checking overlaps of nominal rewriting rules
• Nominal unification
• A formalisation of nominal C-matching through unification with protected variables
• Nominal rewriting
• Nominal Confluence Tool
• Nominal Sets
• Conservative Concurrency in Haskell
• Nominal Completion for Rewrite Systems with Binders
• A Certified Functional Nominal C-Unification Algorithm
• Confluence of orthogonal nominal rewriting systems revisited
• Computer Science Logic
• An Efficient Nominal Unification Algorithm
• General Bindings and Alpha-Equivalence in Nominal Isabelle