Set constraints are the monadic class

Leo Bachmair, Harald Ganzinger, and Uwe Waldmann

In Eighth Annual IEEE Symposium on Logic in Computer Science, pages 75-83, Montreal, Canada, June 19-23, 1993. IEEE Computer Society Press.

Earlier version: Technical Report MPI-I-92-240, Max-Planck-Institut für Informatik, Saarbrücken, December 1992.

Abstract: We investigate the relationship between set constraints and the monadic class of first-order formulas and show that set constraints are essentially equivalent to the monadic class. From this equivalence we can infer that the satisfiability problem for set constraints is complete for NEXPTIME. More precisely, we prove that this problem has a lower bound of NTIME(c^(n/log n)). The relationship between set constraints and the monadic class also gives us decidability and complexity results for certain practically useful extensions of set constraints, in particular "negative" projections and subterm equality tests.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 2003-02-06.
Imprint | Data Protection