Logic in Computer Science (LICS 2000)

Paper: The Role of Decidability in First Order Separations over Classes of Finite Structures (at LICS 2000)

Authors: Steven Lindell Scott Weinstein

Abstract

We establish that the decidability of the first order theory of a class of finite structures C is a simple and useful condition for guaranteeing that the expressive power of FO + LFP properly extends that of FO on C, unifying separation results for various classes of structures that have been studied. We then apply this result to show that it encompasses certain constructive pebble game techniques which are widely used to establish separations between FO and FO + LFP, and demonstrate that these same techniques cannot succeed in performing separations from any complexity class that contains DLOGTIME.

BibTeX

  @InProceedings{LindellWeinstein-TheRoleofDecidabili,
    author = 	 {Steven Lindell and Scott Weinstein},
    title = 	 {The Role of Decidability in First Order Separations over Classes of Finite Structures},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {45--50},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }