Finite Model Theory of the Triguarded Fragment and Related Logics

From International Center for Computational Logic

Toggle side column

Finite Model Theory of the Triguarded Fragment and Related Logics

Emanuel KierońskiEmanuel Kieroński,  Sebastian RudolphSebastian Rudolph
Emanuel Kieroński, Sebastian Rudolph
Finite Model Theory of the Triguarded Fragment and Related Logics
Proceedings of the 36th Annual Symposium on Logic in Computer Science (LICS 2021), to appear
  • KurzfassungAbstract
    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.
  • Projekt:Project: DeciGUT
  • Forschungsgruppe:Research Group: Computational Logic
@inproceedings{KR2021,
  author    = {Emanuel Kiero{\'{n}}ski and Sebastian Rudolph},
  title     = {Finite Model Theory of the Triguarded Fragment and Related Logics},
  booktitle = {Proceedings of the 36th Annual Symposium on Logic in Computer
               Science (LICS 2021)},
  year      = {2021}
}