Layer Systems for Proving Confluence

Authors Bertram Felgenhauer, Harald Zankl, Aart Middeldorp

Thumbnail PDF


  • Filesize: 0.56 MB
  • 12 pages

Document Identifiers

Author Details

Bertram Felgenhauer
Harald Zankl
Aart Middeldorp

Cite AsGet BibTex

Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp. Layer Systems for Proving Confluence. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 288-299, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


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.
  • Term rewriting
  • Confluence
  • Modularity
  • Persistence


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail