%0 Conference Paper %1 Rudolph2018-iy %A Rudolph, Sebastian %A Simkus, Mantas %D 2018 %I EasyChair %K %T The triguarded fragment of first-order logic %X 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.

@inproceedings{Rudolph2018-iy, abstract = {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.}, added-at = {2024-09-10T11:56:37.000+0200}, author = {Rudolph, Sebastian and Simkus, Mantas}, biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/2a529e5bbedd65338de9c05fc3442ce9b/scadsfct}, conference = {LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning}, interhash = {9b403a21817f2bc8a4ae492a45673a57}, intrahash = {a529e5bbedd65338de9c05fc3442ce9b}, keywords = {}, publisher = {EasyChair}, timestamp = {2024-09-10T15:15:57.000+0200}, title = {The triguarded fragment of first-order logic}, year = 2018 }