一句话：研究均匀一维片段中块内交替量词的可满足性，证明两类限制具有有限模型性质且为 NExpTime 完全。
均匀一维片段是一阶逻辑中二变量片段向高阶关系的推广，其量词以同质块出现。本文研究在同一量词块内混合存在与全称量词后片段的可判定性。作者证明两类限制具有有限（指数大小）模型性质，且可满足性问题是 NExpTime 完全的：其一要求每个量词块或纯全称、或以存在量词结尾；其二将变量数限制为三；两者均不允许等词。此外，作者把第二种变体扩展到一个丰富的三变量片段（无等词）子片段，仍保持有限模型性质、可判定且可满足性 NExpTime 完全。
The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime-complete satisfiability.Comment: arXiv admin note: text overlap with arXiv:2310.00994
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FiukK25,
title = {Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic},
author = {Oskar Fiuk and Emanuel Kieronski},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:25)2025}
}