AI summaryⓘ
The authors study how to combine two known logical fragments, the guarded fragment (GF) and the two-variable fragment (FO2), to create a new logical fragment called the triguarded fragment (TGF) that remains decidable for satisfiability. TGF relaxes the standard guardedness rule by only requiring it for parts of formulas with three or more variables. They prove that satisfiability in TGF is decidable with specific complexity bounds and that TGF also has the finite model property, meaning models can be finitely constructed when they exist. However, they note that adding some features, like unrestricted equality, makes the problem undecidable. Their work gives a new, more expressive logical fragment that balances expressiveness and decidability.
first-order logicdecidabilitysatisfiabilityguarded fragmenttwo-variable fragmenttriguarded fragmentfinite model propertypredicate aritydescription logicsmodal logics
Abstract
A prominent research question in computational logic is how to restrict first-order predicate logic (FO) in such a way that the satisfiability problem becomes decidable. Among others, past efforts have identified two prominent decidable FO fragments of high expressivity: the guarded fragment (GF), and the two-variable fragment (FO2). These fragments are of high interest and crucial importance as they provide significant insights into decidability and expressiveness of other prominent (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 article, we show that GF and FO2 can be combined into a new fragment that subsumes both, while maintaining decidability of the satisfiability problem. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF by requiring guardedness of quantification only for subformulae with three or more free variables. We show that, when restricting the use of equality, satisfiability in TGF is N2ExpTime-complete, dropping to NExpTime-complete when the maximum predicate arity is fixed (a natural assumption in the context of MLs and DLs). We further establish that the problem is NP-complete in terms of data complexity, which is again in line with data complexity results for basic expressive DLs. We observe that many natural extensions of TGF, including the liberal use of equality, lead to undecidability. We also establish that TGF has the finite model property (providing a tight doubly exponential bound on the model size), whence finite satisfiability coincides with satisfiability.