Logic in Computer Science (LICS 1999)

Paper: The Two-Variable Guarded Fragment with Transitive Relations (at LICS 1999)

Authors: H. Ganzinger C. Meyer M. Veanes

Abstract

We consider the restriction of the guarded fragment to the two-variable case where, in addition, binary relations may be specified as transitive. We show that (i) this very restricted form of the guarded fragment without equality is undecidable and that (ii) when allowing non-unary relations to occur only in guards, the logic becomes decidable. The latter subclass of the guarded fragment is the one that occurs naturally when translating multi-modal logics of the type K4, S4 or S5 into first-order logic. We also show that the loosely guarded fragment without equality and with a single transitive relation is undecidable.

BibTeX

  @InProceedings{GanzingerMeyerVeane-TheTwoVariableGuard,
    author = 	 {H. Ganzinger and C. Meyer and M. Veanes},
    title = 	 {The Two-Variable Guarded Fragment with Transitive Relations},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {24--34},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }