AI 中文总结
该研究结合一阶谓词逻辑的守卫片段与两变量片段，提出三元守卫片段TGF，证明其可满足性问题在特定条件下的复杂度，且具有有限模型性质，为相关逻辑研究提供新的可判定片段。
AI 中文摘要
计算逻辑领域的一个核心研究问题是如何对一阶谓词逻辑（FO）进行限制，使得其可满足性问题成为可判定的。过往研究已识别出两种高表达性的可判定FO片段：守卫片段（GF）和两变量片段（FO2），这些片段备受关注且至关重要，因为它们为模态逻辑（MLs）、各类描述逻辑（DLs）等其他重要计算逻辑的可判定性与表达性提供了关键洞见，而这些逻辑在验证、知识表示等领域处于核心地位。本文证明，GF和FO2可结合为一个新片段，该片段同时包含两者且保持可满足性问题的可判定性，这个名为三元守卫片段（记为TGF）的片段，是通过放宽GF的标准定义得到的，仅要求对包含三个及以上自由变量的子公式应用量化守卫性。我们证明，当限制等号的使用时，TGF的可满足性问题是N2ExpTime完全的；当谓词最大元数固定（这是MLs和DLs领域的自然假设）时，问题复杂度降至NExpTime完全。我们进一步确定，该问题的数据复杂度为NP完全，这与基础表达性DLs的数据复杂度结果一致。我们还观察到，TGF的许多自然扩展（包括自由使用等号）会导致不可判定性，同时我们证明TGF具有有限模型性质，给出了模型大小的紧双指数界，因此有限可满足性与可满足性等价。
英文摘要
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.
