Logic in Computer Science (LICS 1996)

Paper: Tarskian Set Constraints (at LICS 1996)

Authors: David A. McAllester Robert Givan Carl Witty Dexter Kozen

Abstract

We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning of a Tarskian function symbol is interpreted in an arbitrary first order structure. We show that satisfiability of Tarskian set constraints is decidable in nondeterministic doubly exponential time. We also give complexity results and open problems for various extensions of the language.

BibTeX

  @InProceedings{McAllesterGivanWitt-TarskianSetConstrai,
    author = 	 {David A. McAllester and Robert Givan and Carl Witty and Dexter Kozen},
    title = 	 {Tarskian Set Constraints},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {138-147},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }