2026-07-22T18:25:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5201 2024-03-06T10:36:03Z ddc:004 open_access

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules Nagele, Julian Felgenhauer, Bertram Middeldorp, Aart term rewriting confluence automation transformation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Julian Nagele and Bertram Felgenhauer and Aart Middeldorp 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.257 urn:nbn:de:0030-drops-52010 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.257 eng https://creativecommons.org/licenses/by/3.0/legalcode