[Back]

S. Rudolph, M. Simkus:
"The Triguarded Fragment of First-Order Logic";
Talk: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018", EasyChair EPiC Series in Computing, 57 (2018), 604 - 619.

Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are of crucial importance because they provide significant insights into decidabil- ity and expressiveness of other (computational) logics like Modal Logics (MLs) and various Description Logics (DLs), which play a central role in Verification, Knowledge Represen- tation, and other areas. In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them 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, in the absence of equality, satisfiability in 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 MLs and DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.

complexity, decidability, Description Logics, fragments of first-order logic, modal logic, The guarded fragment, The two-variable fragment

https://easychair.org/publications/open/wlJ3