Improving automatic confluence analysis of rewrite systems by redundant rules
View/ Open
Volume
36
Pagination
257 - 268
ISBN-13
9783939897859
DOI
10.4230/LIPIcs.RTA.2015.257
ISSN
1868-8969
Metadata
Show full item recordAbstract
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.