Checking overlaps of nominal rewriting rules

DOI10.1016/j.entcs.2016.06.004zbMath1401.68131OpenAlexW2463026518WikidataQ113317685 ScholiaQ113317685MaRDI QIDQ1744404

Mauricio Ayala-Rincón, Murdoch James Gabbay, Ana Cristina Rocha-Oliveira, Maribel Fernández

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.004

zbMATH Keywords

confluencerewritingnominal syntaxbinding

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (7)

Confluence of orthogonal term rewriting systems in the prototype verification system ⋮ Nominal unification with atom-variables ⋮ Nominal syntax with atom substitutions ⋮ Unnamed Item ⋮ Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting ⋮ Rewriting with generalized nominal unification ⋮ Confluence and commutation for nominal rewriting systems with atom-variables

Cites Work

• Unnamed Item
• Unnamed Item
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• Matching and alpha-equivalence check for nominal terms
• Higher-order rewrite systems and their confluence
• Combinatory reduction systems: Introduction and survey
• Nominal unification
• Nominal rewriting
• On theories with a combinatorial definition of 'equivalence'
• Relating Nominal and Higher-Order Rewriting
• Nominal Completion for Rewrite Systems with Binders
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Confluence of orthogonal nominal rewriting systems revisited
• Automata, Languages and Programming
• Tree-Manipulating Systems and Church-Rosser Theorems

This page was built for publication: Checking overlaps of nominal rewriting rules