The Two-Variable Guarded Fragment with Transitive Guards Is 2EXPTIME-Hard
Emanuel Kieroński5 
| (5) |
Institute of Computer Science University of Wroc law, ul.Przesmyckiego 20, 51-151 Wroc law, Poland |
Abstract
We prove that the satisfiability problem for the two-variable guarded fragment with transitive guards GF
2+TG 2EXPTIME-hard. This result closes the open questions left in [4],[17].In fact,we show 2EXPTIME-hardness of min
GF
2 +TG a fragment of GF
2 +TG with- out equality and with just one transitive relation .,which is the only non-unary symbol allowed. Our lower bound for
min
GF
2 +TG the upper bound for the whole guarded fragment with transitive guards and the unrestricted number of variables GF +TG by Szwast and Tendera [17 ],so in fact GF
2+TG 2EXPTIME-complete. It is surpris- ing that the complexity of min
GF
2 +TG higher then the complexity of the variant with one-way transitive guards GF
2 +TG [9 ]. The latter logic appears naturally as a counterpart of temporal logics without past operators.
Supported by KBN grant 8 T11C 043 19
By the first order logic we mean in this paper the first order logic without constants and function symbols.
References secured to subscribers.