Decidability of the Guarded Fragment with the Transitive Closure

We consider an extension of the guarded fragment in which one can guard quantiers using the transitive closure of some binary relations. The obtained logic captures the guarded fragment with transitive guards, and in fact extends its expressive power non-trivially, preserving the complexity: we prove that its satisability problem is 2Exptimecomplete.

• Type: Conference
• Year: 2009
• Where: ICALP
• Authors: Jakub Michaliszyn
• Keywords: Binary Relations, ICALP 2009, Programming Languages, Transitive Closure, Transitive Guards