The unification problem for confluent right-ground term rewriting systems
The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a given TRS R and two terms M and N, whether there exists a substitution ? such that M? and N? are congruent modulo R (i.e., M??R*N?). In this paper, the unification problem for confluent right-ground TRSs is shown to be decidable. To show this, the notion of minimal terms is introduced and a new unification algorithm for obtaining a substitution whose range consists of minimal terms is proposed. Our result extends the decidability of unification for canonical (i.e., terminating and confluent) right-ground TRSs given by Hullot [Proceedings of the 5th Conference on Automated Deduction, LNCS, vol. 87, 1980, p. 318] in the sense that the termination condition can be omitted.
unification right-ground term rewriting systems decidability confluence