zbMATH — the first resource for mathematics

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].
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.)
Full Text: DOI