Document Open Access Logo

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules

Authors Julian Nagele, Bertram Felgenhauer, Aart Middeldorp

Thumbnail PDF


  • Filesize: 0.51 MB
  • 12 pages

Document Identifiers

Author Details

Julian Nagele
Bertram Felgenhauer
Aart Middeldorp

Cite AsGet BibTex

Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 257-268, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.
  • term rewriting
  • confluence
  • automation
  • transformation


  • 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