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

fYear

1993

fDate

19-23 Jun 1993

Firstpage

75

Lastpage

83

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

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/LICS.1993.287598

Filename

287598