Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

Paper: Set constraints are the monadic class (at LICS 1993)

Winner of the Test-of-Time Award in 2013
Authors: Leo Bachmair Harald Ganzinger Uwe Waldmann

Abstract

The authors investigate the relationship between set constraints and the monadic class of first-order formulas and show that set constraints are essentially equivalent to the monadic class. From this equivalence, they infer that the satisfiability problem for set constraints is complete for NEXPTIME. More precisely, it is proved that this problem has a lower bound of NTIME(cnlog n/), for some c>0. The relationship between set constraints and the monadic class also gives decidability and complexity results for certain practically useful extensions of set constraints, in particular “negative” projections and subterm equality tests

BibTeX

  @InProceedings{BachmairGanzingerWa-Setconstraintsareth,
    author = 	 {Leo Bachmair and Harald Ganzinger and Uwe Waldmann},
    title = 	 {Set constraints are the monadic class},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {75--83},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2016-01-1416:21
Andrzej Murawski