TY - GEN
T1 - Proving confluence of term rewriting systems automatically
AU - Aoto, Takahito
AU - Yoshida, Junichi
AU - Toyama, Yoshihito
PY - 2009
Y1 - 2009
N2 - We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.
AB - We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.
UR - http://www.scopus.com/inward/record.url?scp=70350649118&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350649118&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-02348-4_7
DO - 10.1007/978-3-642-02348-4_7
M3 - Conference contribution
AN - SCOPUS:70350649118
SN - 3642023479
SN - 9783642023477
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 93
EP - 102
BT - Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings
T2 - 20th International Conference on Rewriting Techniques and Applications, RTA 2009
Y2 - 29 June 2009 through 1 July 2009
ER -