On the Restraining Power of Guards
On the Restraining Power of Guards
复制标题
论看守人员的约束力
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
E. Grädel
中科院分区：
文献类型：
--
作者：
E. Grädel
一阶逻辑的受保护片段最近由安德烈卡、货车本瑟姆和内梅蒂介绍;它们由关系一阶公式组成，其量词被原子适当地相对化。这些片段是有趣的，因为它们以一种自然的方式扩展了许多命题模态逻辑，因为它们具有有用的模型论性质，特别是因为它们是可判定类，避免了几乎所有其他已知的一阶逻辑可判定片段的常见语法限制（关于关系符号的arity，量词模式或变量的数量）。在这里，我们研究这些片段的计算复杂性。证明了一阶逻辑的保护片段（GF）和松保护片段（LGF）的可满足性问题对于确定性双指数时间是完全的。对于只有有限数量的变量或只有有限数量的关系符号的子片段，可满足性是Exptime完全的。我们进一步建立了保护片段和松保护片段的树模型性质，并证明了保护片段的有限模型性质。它还表明，一些自然的，适度的扩展的保护片段是不可判定的。
Abstract Guarded fragments of first-order logic were recently introduced by Andréka, van Benthem and Németi; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is Exptime-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable.