@TechReport{Niehren_et_al:1998,
AUTHOR = {Niehren, Joachim and Müller, Martin and Talbot, JeanMarc},
TITLE = {Entailment of Atomic Set Constraints is PSPACEComplete},
YEAR = {1998},
ADDRESS = {Saarbrücken},
TYPE = {Technical Report},
INSTITUTION = {Universität des Saarlandes, Programming Systems Lab},
URL = {www.ps.unisb.de/Papers/abstracts/atomiclics99.html ftp://ftp.ps.unisb.de/pub/papers/ProgrammingSysLab/atomic:98.ps.gz},
ABSTRACT = {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 $t_1subseteq t_2$ between firstorder terms without set operators. It is wellknown 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 quantified boolean formulas and is thus PSPACE hard. For infinite signatures, we also present a PSPACEalgorithm for solving atomic set constraints with negation. This proves that entailment of atomic set constraints is PSPACEcomplete for infinite signatures. In case of finite signatures, the problem is even DEXPTIMEhard.},
ANNOTE = {COLIURL : Niehren:1998:EAS.pdf Niehren:1998:EAS.ps} }
