MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

MPI-I-92-240

Set constraints are the Monadic class

Ganzinger, Harald and Bachmair, Leo and Waldmann, Uwe

December 1992, 13 pages.

.
Status: available - back from printing

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.

  • MPI-I-92-240.pdfMPI-I-92-240.pdfMPI-I-92-240.dvi
  • Attachement: MPI-I-92-240.dvi (58 KBytes); MPI-I-92-240.pdf (122 KBytes)

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-240

Hide details for BibTeXBibTeX
@TECHREPORT{GanzingerBachmairWaldmann92,
  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},
}