COMPLETION OF REWRITE SYSTEMS WITH MEMBERSHIP CONSTRAINTS PART II - CONSTRAINT SOLVING

We consider a constraint system involving equations and membership con straints. Membership constraints are interpreted as the membership to some recognizable tree languages. The terms may contain a restricted k ind of context variables. We give a set of constraint solving rules wh ich is proved to be complete and terminating. This gives a unification algorithm for an order-sorted logic (without any restriction on the s ignature) which contains some restricted kind of second-order variable s. (C) 1998 Academic Press Limited.