On rewrite constraints and context unification
We show that stratified context unification, which is one of the most expressive fragments of context unification known to be decidable, is equivalent to the satisfiability problem of slightly generalized rewriting constraints. (C) 2000 Elsevier Science B.V. All rights reserved.
rewrite constraints unification automatic theorem proving theory of computation