Abstract

We introduce layer systems for proving generalizations of the modularity of
confluence for first-order rewrite systems. Layer systems specify how terms
can be divided into layers. We establish structural conditions on those
systems that imply confluence. Our abstract framework covers known results
like many-sorted persistence, layer-preservation and currying. We present a
counterexample to an extension of the former to order-sorted rewriting and
derive new sufficient conditions for the extension to hold.

BibTeX

@inproceedings{BFHZAM-FSTTCS11,
  author    = "Bertram Felgenhauer and Harald Zankl and Aart Middeldorp",
  title     = "Layer Systems for Proving Confluence",
  booktitle = "Proceedings of the 30th IARCS Annual Conference on
               Foundations of Software Technology and Theoretical Computer
               Science",
  address   = "Mumbai",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 13,
  pages     = "288--299",
  year      = 2011
}