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
- Location: APB 3027
- Start: 29. November 2018 at 1:00 pm
- End: 29. November 2018 at 2:30 pm
- Research group: Computational Logic
- Event series: KBS Seminar
- iCal
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.
