Finite Model Theory of the Triguarded Fragment and Related Logics
Logic in Computer Science
2021-01-26 v2 Artificial Intelligence
Computational Complexity
Logic
Abstract
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.
Keywords
Cite
@article{arxiv.2101.08377,
title = {Finite Model Theory of the Triguarded Fragment and Related Logics},
author = {Emanuel Kieroński and Sebastian Rudolph},
journal= {arXiv preprint arXiv:2101.08377},
year = {2021}
}