Title :
Set constraints are the monadic class
Author :
Bachmair, Leo ; Ganzinger, Harald ; Waldmann, Uwe
Author_Institution :
Dept. of Comput. Sci., State Univ. of New York, Stony Brook, NY, USA
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(cnlog 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
Keywords :
computational complexity; constraint theory; decidability; set theory; NEXPTIME; NTIME; completeness; complexity; decidability; equivalence; first-order formulas; lower bound; monadic class; negative projections; satisfiability problem; set constraints; subterm equality tests; Abstracts; Algorithm design and analysis; Computer languages; Computer science; Concrete; Constraint theory; Inference algorithms; Logic programming; Testing; Vocabulary;
Conference_Titel :
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-8186-3140-6
DOI :
10.1109/LICS.1993.287598
