"Negative Set Constraints with Equality" by Witold Charatonik and
 Leszek Pacholski

<BR>
<BR>


Abstract:

<P>
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  and A.Aiken, D.Kozen, and
E.L.Wimmers. However, both these proofs are  long, involved
and do not seem to extend to more general set constraints.
<BR>
<BR>

Our approach is based on a reduction of set constraints to the 
monadic class given in a recent paper by L.Bachmair, H.Ganzinger, 
and U.Waldmann.
We first give a new proof of decidability of 
systems of mixed positive and negative set constraints. 
We explicitely 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 NEXPTIME. 
</P>
<BR>
<BR>
The full problem was solved in:

<P> 

Witold Charatonik, Leszek Pacholski,<A
HREF="http://swarog.ii.uni.wroc.pl/~wch/papers/focs94.html"> Set
constraints with projections are in NEXPTIME</A>, Proceedings of the
35th Annual Symposium on Foundations of Computer Science (FOCS), Santa
Fe 1994 </P>

  <A Href="lics94.ps">
  postscript file (138K)</A>,
  <A Href="lics94.dvi">
  dvi file (59K)</A>, or 
  <A Href="lics94.ps.Z">
  compressed postscript file (66K)</A>