TY - GEN
T1 - Disproving confluence of term rewriting systems by interpretation and ordering
AU - Aoto, Takahito
PY - 2013
Y1 - 2013
N2 - In order to disprove confluence of term rewriting systems, we develop new criteria for ensuring non-joinability of terms based on interpretation and ordering. We present some instances of the criteria which are amenable for automation, and report on an implementation of a confluence disproving procedure based on these instances. The experiments reveal that our method is successfully applied to automatically disprove confluence of some term rewriting systems, on which state-of-the-art automated confluence provers fail. A key idea to make our method effective is the introduction of usable rules - this allows one to decompose the constraint on rewrite rules into smaller components that depend on starting terms.
AB - In order to disprove confluence of term rewriting systems, we develop new criteria for ensuring non-joinability of terms based on interpretation and ordering. We present some instances of the criteria which are amenable for automation, and report on an implementation of a confluence disproving procedure based on these instances. The experiments reveal that our method is successfully applied to automatically disprove confluence of some term rewriting systems, on which state-of-the-art automated confluence provers fail. A key idea to make our method effective is the introduction of usable rules - this allows one to decompose the constraint on rewrite rules into smaller components that depend on starting terms.
KW - Confluence
KW - Interpretation
KW - Non-Joinability
KW - Ordering
KW - Term Rewriting Systems
UR - http://www.scopus.com/inward/record.url?scp=84886770815&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84886770815&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40885-4_22
DO - 10.1007/978-3-642-40885-4_22
M3 - Conference contribution
AN - SCOPUS:84886770815
SN - 9783642408847
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 311
EP - 326
BT - Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings
T2 - 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013
Y2 - 18 September 2013 through 20 September 2013
ER -