Confluence and commutation for nominal rewriting systems with atom-variables

DOI10.1007/978-3-030-68446-4_3OpenAlexW3131179554MaRDI QIDQ2119102

Kentaro Kikuchi, Takahito Aoto

Publication date: 23 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_3

zbMATH Keywords

confluencecommutationvariable bindingnominal unificationalpha-equivalencenominal rewritingatom-variable

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• How to prove equivalence of term rewriting systems without induction
• Nominal unification with atom-variables
• Parallel closure theorem for left-linear nominal rewriting systems
• Checking overlaps of nominal rewriting rules
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Nominal Confluence Tool
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Rewriting with generalized nominal unification
• Confluence of orthogonal nominal rewriting systems revisited
• On the Church-Rosser property for the direct sum of term rewriting systems
• Tree-Manipulating Systems and Church-Rosser Theorems
• Confluence without termination via parallel critical pairs

This page was built for publication: Confluence and commutation for nominal rewriting systems with atom-variables