TY - GEN
T1 - Ground confluence prover based on rewriting induction
AU - Aoto, Takahito
AU - Toyama, Yoshihito
N1 - Funding Information:
Thanks are due to the anonymous reviewers for helpful comments. This work is partially supported by JSPS KAKENHI Nos. 15K00003, 25280025.
Publisher Copyright:
© 2016 Takahito Aoto and Yoshihito Toyama.
PY - 2016/6/1
Y1 - 2016/6/1
N2 - Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems.
AB - Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems.
KW - Ground confluence
KW - Non-orientable equations
KW - Rewriting induction
KW - Term rewriting systems
UR - http://www.scopus.com/inward/record.url?scp=84977589981&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84977589981&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2016.33
DO - 10.4230/LIPIcs.FSCD.2016.33
M3 - Conference contribution
AN - SCOPUS:84977589981
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
A2 - Kesner, Delia
A2 - Pientka, Brigitte
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Y2 - 22 June 2016 through 26 June 2016
ER -