Logic in Computer Science (LICS 1999)

Paper: Entailment of Atomic Set Constraints is PSPACE-Complete (at LICS 1999)

Authors: Joachim Niehren Martin Müller Jean-Marc Talbot

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 1\matht 2 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 decid-able 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.

BibTeX

  @InProceedings{NiehrenMllerTalbot-EntailmentofAtomicS,
    author = 	 {Joachim Niehren and Martin Müller and Jean-Marc Talbot},
    title = 	 {Entailment of Atomic Set Constraints is PSPACE-Complete},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {285--294},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }