[Back]

S. Rudolph, M. Simkus:
"Satisfiability in the Triguarded Fragment of First-Order Logic";
Talk: 31st International Workshop on Description Logics (DL 2018), Tempe, Arizona, USA; 10-27-2018 - 10-29-2018; in: "Proceedings of the 31st International Workshop on Description Logics co-located with 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), Tempe, Arizona, US, October 27th - to - 29th, 2018.", CEUR-WS.org, (2018), Paper ID 32, 12 pages.

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.

http://ceur-ws.org/Vol-2211/paper-32.pdf