The triguarded fragment of first-order logic.

*(English)*Zbl 1416.03008
Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 604-619 (2018).

Summary: Past research into decidable fragments of first-order logic (\(\mathbb{FO}\)) has produced two very prominent fragments: the guarded fragment \(\mathbb{GF}\), and the two-variable fragment \(\mathbb{FO}^2\). These fragments are of crucial importance because they provide significant insights into decidability and expressiveness of other (computational) logics like modal logics (MLs) and various description logics (DLs), which play a central role in verification, knowledge representation, and other areas. In this paper, we take a closer look at \(\mathbb{GF}\) and \(\mathbb{FO}^2\), and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted \(\mathbb{TGF}\)), is obtained by relaxing the standard definition of \(\mathbb{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 \(\mathbb{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 \(\mathbb{TGF}\), including the addition of equality, lead to undecidability.

For the entire collection see [Zbl 1407.68021].

For the entire collection see [Zbl 1407.68021].

##### MSC:

03B20 | Subsystems of classical logic (including intuitionistic logic) |

03B25 | Decidability of theories and sets of sentences |

03B45 | Modal logic (including the logic of norms) |

68T27 | Logic in artificial intelligence |

68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |