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 :
بازگشت