Satisfiability in the Triguarded Fragment of First-Order Logic

From International Center for Computational Logic

Satisfiability in the Triguarded Fragment of First-Order Logic

Talk by Sebastian Rudolph
Abstract: Most Description Logics (DLs) can be translated into well-known decidable fragments of first-order logic FO, including the guarded fragment GF and the two-variable fragment FO2. Given their prominence in DL research, we take closer look at GF and FO2, and present a new fragment that subsumes both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that satisfiability of equality-free TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.


This talk is a presentation given at the 31st International Workshop on Description Logics, 2018.