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

*Winner of the Test-of-Time Award in 2013***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^{n}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 Symposium on Logic in Computer Science (LICS 1993)}, year = {1993}, month = {June}, pages = {75--83}, location = {Montreal, Canada}, publisher = {IEEE Computer Society Press} }