# Publication details

##
Entailment of Atomic Set Constraints is PSPACE-Complete

Martin Müller, Joachim Niehren, Jean-Marc Talbot

Fourteenth Annual IEEE Symposium on Logic in Computer Sience, pp. 285--294, IEEE Press, 1999

The complexity of set constraints has been extensively studied over the last years and was often found quite high. At the lower end of
expressiveness, there are atomic set constraints which are
conjunctions of inclusions t1 $subseteq$ t2
between first-order terms
without set operators. It is well-known that satisfiability of atomic
set constraints can be tested in cubic time. Also, entailment of
atomic set constraints has been claimed decidable in polynomial
time. We refute this claim. We show that entailment between atomic set
constraints can express validity of quantified boolean
formulas and is thus PSPACE hard. For infinite signatures, we also
present a PSPACE-algorithm for solving atomic set constraints with
negation. This proves that entailment of atomic set constraints is
PSPACE-complete for infinite signatures. In case of finite
signatures, this problem is even DEXPTIME-hard.

Download PDF
Show BibTeX

@INPROCEEDINGS{atomic-lics-99,
title = {Entailment of Atomic Set Constraints is PSPACE-Complete},
author = {Martin Müller and Joachim Niehren and Jean-Marc Talbot},
year = {1999},
month = {{2--5, July}},
publisher = {{IEEE Press}},
booktitle = {Fourteenth Annual IEEE Symposium on Logic in Computer Sience},
pages = {{285--294}},
address = {{ Trento, Italy}},
note = {{An extended version is available at \url{www.ps.uni-sb.de/Papers/abstracts/atomic:98.html}}},
}

Login to edit

Legal notice, Privacy policy