Satisfiability in the Triguarded Fragment of First-Order Logic
Aus International Center for Computational Logic
Satisfiability in the Triguarded Fragment of First-Order Logic
Vortrag von Sebastian Rudolph
- Veranstaltungsort: APB 3027
- Beginn: 29. November 2018 um 13:00
- Ende: 29. November 2018 um 14:30
- Forschungsgruppe: 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.
