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
Link To Document