Proving Confluence of Term Rewriting Systems Automatically

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), laver-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.