Negative set constraints with equality

Systems of set constraints describe relations between sets of ground terms. They have been successfully used in program analysis and type inference. So far two proofs of decidability of mixed set constraints have been given: by R. Gilleron, S. Tison and M. Tommasi (1993) and A. Aiken, D. Kozen, and E.L. Wimmers (1993). However, both these proofs are long, involved and do not seem to extend to more general set constraints. Our approach is based on a reduction of set constraints to the monadic class given in a paper by L. Bachmair, H. Ganzinger, and U. Waldmann (1993). We first give a new proof of decidability of systems of mixed (positive and negative) set constraints. We explicitly describe a very simple algorithm working in NEXPTIME and we give in all detail a relatively easy proof of its correctness. Then, we sketch how our technique can be applied to get various extensions of this result. In particular we prove that the problem of consistency of mixed set constraints with restricted projections and unrestricted diagonalization is in NEXPTIME