The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.
翻译:三维保护碎片(TGF)是一阶逻辑中最清晰的分层碎片之一,它无一例外地将两种可变和有守卫的碎片混合在一起,我们证明TGF具有有限的模型属性(根据模型大小提供一个紧密的双倍指数),因此,有限的可控性与已知的N2ExplentTime-complete相符。我们利用类似的构思,还建立了2个无固定(三)保护的碎片的有限可控性,由中转警卫组成。