Rewriting with generalized nominal unification

DOI10.1017/S0960129520000122MaRDI QIDQ5139280zbMATH OpenOpenAlexFDO

Authors Yunus D. K. Kutz, Manfred Schmidt-Schauß

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) Grammars and rewriting systems (68Q42) Logic in computer science (03B70)

Recommendations

• Confluence of orthogonal nominal rewriting systems revisited
• Implementing nominal unification
• Automata, Languages and Programming
• Nominal syntax with atom substitutions: matching, unification, rewriting
• Nominal confluence tool

Cites work

• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A certified functional nominal C-unification algorithm
• A formalisation of nominal C-matching through unification with protected variables
• A polynomial nominal unification algorithm
• An efficient nominal unification algorithm
• Checking overlaps of nominal rewriting rules
• Computer Science Logic
• Confluence of orthogonal nominal rewriting systems revisited
• Conservative concurrency in Haskell
• Equivariant unification
• General bindings and alpha-equivalence in Nominal Isabelle
• Nominal completion for rewrite systems with binders
• Nominal confluence tool
• Nominal rewriting
• Nominal sets. Names and symmetry in computer science
• Nominal techniques in Isabelle/HOL
• Nominal unification
• Nominal unification with atom-variables
• Parallel closure theorem for left-linear nominal rewriting systems

Cited in

(11)

• Nominal confluence tool
• Nominal unification with letrec and environment-variables
• Confluence and commutation for nominal rewriting systems with atom-variables
• Nominal completion for rewrite systems with binders
• Nominal unification with atom-variables
• Checking overlaps of nominal rewriting rules
• Term Rewriting and Applications
• Nominal rewriting
• Parallel closure theorem for left-linear nominal rewriting systems
• Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting
• Confluence of orthogonal nominal rewriting systems revisited

Describes a project that uses

Uses Software

• Nominal Isabelle
• Haskell

This page was built for publication: Rewriting with generalized nominal unification

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