• DocumentCode
    3036603
  • Title

    The two-variable guarded fragment with transitive relations

  • Author

    Ganzinger, H. ; Meyer, C. ; Veanes, M.

  • Author_Institution
    Max-Planck-Inst. fur Inf., Saarbrucken, Germany
  • fYear
    1999
  • fDate
    1999
  • Firstpage
    24
  • Lastpage
    34
  • 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 fragments the one that occurs naturally when translating multi-modal logics of the type Kg4 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
  • Keywords
    decidability; formal logic; binary relations; decidability; first-order logic; multi-modal logics; transitive relations; two-variable guarded fragment; Logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1999. Proceedings. 14th Symposium on
  • Conference_Location
    Trento
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-0158-3
  • Type

    conf

  • DOI
    10.1109/LICS.1999.782582
  • Filename
    782582