Just as saturation under an appropriate superposition calculus leads to a convergent presentation of a given equational theory, saturation under a suitable chaining calculus gives, what we call, a rewrite closure. We present a theorem that characterizes confluence of (possibly nonterminating) term rewrite systems that admit a rewrite closure presentation, in terms of local confluence of a related terminating term rewrite system and joinability inclusion between these two rewrite systems. Using constraints to avoid variable chaining, we obtain a finite and computable rewrite closure presentation for right ground systems. This gives an alternate method to decide the reachability and joinability properties for right ground systems. The characterization of confluence, combined with the rewrite closure presentation, is used to obtain a decision procedure for confluence of right ground systems (this problem has been open for quite some time 8), and a simple decision procedure for the unification problem of confluent right ground systems (result recently obtained in 17). An EXPTIME-hardness result is also proved for reachability and confluence of right ground systems.
展开▼
