Completion of Rewrite Systems with Membership Constraints Part II: Constraint Solving

We consider a constraint system involving equations and membership constraints. Membership constraints are interpreted as the membership to some recognizable tree languages. The terms may contain a restricted kind ofcontext variables. We give a set of constraint solving rules which is proved to be complete and terminating. This gives a unification algorithm for an order-sorted logic (without any restriction on the signature) which contains some restricted kind of second-order variables.