Finite Model Theory of the Triguarded Fragment and Related Logics
This provides foundational theoretical results for logics used in knowledge representation and verification, though it is incremental as it builds on known decidability.
The paper tackled the finite model property for the Triguarded Fragment (TGF) of first-order logic, showing it has a doubly exponential bound on model size and that finite satisfiability is N2ExpTime-complete, with similar results for related logics.
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.