Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Set constraints are the Monadic class

Ganzinger, Harald and Bachmair, Leo and Waldmann, Uwe

MPI-I-92-240. December 1992, 13 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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 ${\rm 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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-92-240.pdfMPI-I-92-240.pdfMPI-I-92-240.dvi58 KBytes; 122 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Ganzinger, Harald and Bachmair, Leo and Waldmann, Uwe},
  TITLE = {Set constraints are the Monadic class},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-240},
  MONTH = {December},
  YEAR = {1992},
  ISSN = {0946-011X},