Finite Model Theory of the Triguarded Fragment and Related Logics.

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

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.

Details

Original languageEnglish
Title of host publication2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
Pages1-13
Number of pages13
ISBN (electronic)9781665448956
Publication statusPublished - 29 Jun 2021
Peer-reviewedYes

External IDs

Scopus 85112209706
Mendeley 5d6a0c73-dfce-36ca-a00d-6a3413dc8a04

Keywords

ASJC Scopus subject areas