Set Constraints in Some Equational Theories

AbstractSet constraints are relations between sets of ground terms over a given alphabet. They give a natural formalism for many problems in program analysis, type inference, order-sorted unification, and constraint logic programming. In this paper we start studies of set constraints in the environment given by equational specifications. We show that in the case of associativity (i.e., in free monoids) as well as in the case of associativity and commutativity (i.e., in commutative monoids) the problem of consistency of systems of set constraints is undecidable; in linear nonerasing shallow theories the consistency of systems of positive set constraints is NEXPTIME-complete and in linear shallow theories the problem for positive and negative set constraints is decidable