We show that the confluence of shallow linear term rewrite systems is decidable. The decision procedure is a nontrivial generalization
of the polynomial time algorithms for deciding confluence of ground and restricted non-ground term rewrite systems presented
in [13]
Partially supported by the Spanish CICYT project MAVERISH ref. TIC2001-2476-C03-01.
Research supported in part by DARPA under the MoBIES and SEC programs administered by AFRL under contracts F33615-00-C-1700
and F33615-00-C-3043, and NSF CCR-0082560.
Research supported in part by NSF grant CCR-9732186.