Entailment of Atomic Set Constraints is PSPACE-Complete

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 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.
Type de document :
Communication dans un congrès
Fourteenth Annual IEEE Symposium on Logic in Computer Sience, 1999, Trento, Italy. IEEE Computer Science Press, pp.285--294, 1999
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00536817
Contributeur : Joachim Niehren <>
Soumis le : jeudi 18 novembre 2010 - 17:32:03
Dernière modification le : mardi 24 avril 2018 - 13:37:27
Document(s) archivé(s) le : samedi 19 février 2011 - 02:50:56

Fichiers

atomic-lics-99.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00536817, version 1

Collections

Citation

Joachim Niehren, Martin Müller, Jean-Marc Talbot. Entailment of Atomic Set Constraints is PSPACE-Complete. Fourteenth Annual IEEE Symposium on Logic in Computer Sience, 1999, Trento, Italy. IEEE Computer Science Press, pp.285--294, 1999. 〈inria-00536817〉

Partager

Métriques

Consultations de la notice

146

Téléchargements de fichiers

101