Finite Model Theory of the Triguarded Fragment and Related Logics

From International Center for Computational Logic

Finite Model Theory of the Triguarded Fragment and Related Logics

Talk by Sebastian Rudolph
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.


This talk will take place online via BigBlueButton. To access the room, take one of the following links:

with ZIH-login:

https://selfservice.zih.tu-dresden.de/l/link.php?m=128248&p=fac3a576

without ZIH-login:

https://selfservice.zih.tu-dresden.de/link.php?m=128248&p=9f228a78