We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of ``nice'' models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is ${\rm T{\small OWER}}$-complete. If only two variable are used, computational complexity drops to ${\rm NE{\small XP}T{\small IME}}$-completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, $\Pi^0_1$- and $\Sigma^0_1$-complete. Additionally, satisfiability becomes $\Sigma^1_1$-complete if periodic counting quantifiers are permitted.
翻译:我们研究一阶逻辑的长笛片段,该片段通常被视为对多种缺乏角色逆的描述逻辑系统的多变量非保护扩展。本文证明,可满足的长笛语句(即使在合理的扩展下)允许一类特殊的"良好"模型,我们称之为全局/局部齐次模型。齐次模型使我们能够简化分析带计数量词的长笛逻辑的方法,并为带周期性计数的长笛片段(有限)可满足性问题的可判定性建立了新的结果。具体而言,我们将证明该语言的(有限)可满足性问题是${\rm T{\small OWER}}$完全的。若仅使用两个变量,计算复杂度将降至${\rm NE{\small XP}T{\small IME}}$完全。我们进一步证明,长笛逻辑的泛化形式(如相邻片段)的有限可满足性问题与一般可满足性问题分别是$\Pi^0_1$完全与$\Sigma^0_1$完全的。若允许周期性计数量词,可满足性问题将变为$\Sigma^1_1$完全的。