Logic in Computer Science (LICS 1993)

Paper: Set constraints are the monadic class (at LICS 1993)

Authors: Leo Bachmair Harald Ganzinger Uwe Waldmann

Abstract

The authors 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, they infer that the satisfiability problem for set constraints is complete for NEXPTIME. More precisely, it is proved that this problem has a lower bound of NTIME(cⁿlog n/), for some c>0. The relationship between set constraints and the monadic class also gives decidability and complexity results for certain practically useful extensions of set constraints, in particular “negative” projections and subterm equality tests

BibTeX

  @InProceedings{BachmairGanzingerWa-Setconstraintsareth,
    author = 	 {Leo Bachmair and Harald Ganzinger and Uwe Waldmann},
    title = 	 {Set constraints are the monadic class},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {75--83},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }