Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 26th International Conference on Rewriting Techniques
and Applications (RTA 2015), Leibniz International Proceedings in
Informatics 36, pp. 257 – 268, 2015.
Abstract
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.BibTeX Entry
@inproceedings{NFM-RTA15,
author = "Julian Nagele and Bertram Felgenhauer and Aart Middeldorp",
title = "Improving Automatic Confluence Analysis of Rewrite Systems
by Redundant Rules",
booktitle = "Proceedings of the 26th International Conference on Rewriting
Techniques and Applications",
editor = "Maribel Fern\'andez",
series = "Leibniz International Proceedings in Informatics"
volume = 36,
pages = "257--268",
year = 2015,
doi = "10.4230/LIPIcs.RTA.2015.257"
}