Automatically proving confluence of non-terminating rewrite systems via a generalized Newman-style approach

Confluence is, besides termination, the most fundamental property of (term) rewrite systems. For a long time it is well-known how to prove confluence of terminating systems via Newman's Lemma. Yet, for non-terminating rewrite systems confluence criteria and proof techniques are very rare and notoriously difficult to obtain. Here we present a new approach in this direction. Our main result is a generalized version of Newman's Lemma for left-linear rewrite systems that does not need a full termination assumption. We discuss its relationships to previous confluence criteria, its restrictions,examples of application as well as open problems. The whole approach is developed in the (more general) framework of context-sensitive rewriting which thus turns out to be useful also for ordinary (context-free) rewriting.
In the talk, which is based on recent joint work with Salvador Lucas (Valencia, Spain), we will start with an overview of known confluence criteria for (possibly) non-terminating rewrite systems.