Portal de Periódicos da CAPES

EXPSPACE-Complete Variant of Guarded Fragment with Transitivity

2002; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-45841-7_50

1611-3349

Emanuel Kieroński,

Algorithms and Data Compression

We introduce a new fragment GF 2 + $$ \overrightarrow {TG} $$ of the first order logic — the two-variable guarded fragment with one-way transitive guards. This logic corresponds in a natural way to temporal logics without past operators. We prove that the satisfiability problem for GF+ $$ \overrightarrow {TG} $$ is EXPSPACE-complete. The lower bound, obtained for the monadic version of the considered logic without equality, improves NEXPTIME lower bound for the whole two-variable guarded fragment with transitive guards GF 2 + TG, given by Szwast and Tendera [8].