修正了Promise模板模型检验问题
Fixed-Template Promise Model Checking Problems
摘要：
固定模板约束满足问题（CSP）可以看作是判定给定的本原正一阶句在固定结构（也称模型）中是否为真的问题。我们研究了一类问题，推广CSP同时在两个方向：我们固定一组$\mathcal{L}$的量词和布尔连接，我们指定两个版本的每个约束，一个强，一个弱。给定一个只使用$\mathcal{L}$中的符号的句子，任务是区分这个句子在强意义上是真的，还是在弱意义上是假的。我们将这些问题的计算复杂性分类为一阶逻辑的存在正不等式自由片段，即，$\mathcal{L} = \{\exists,\land,\lor\}$，我们证明了一些上界和下界的积极平等的自由片段，$\mathcal{L} = \{\exists,\forall,\land,\lor\}$。部分结果是足够的，例如，对于后一个片段的所有扩展。
英文摘要：
The fixed-template constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive first-order sentence is true in a fixed structure (also called model). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set $\mathcal{L}$ of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from $\mathcal{L}$, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic, i.e., $\mathcal{L} = \{\exists,\land,\lor\}$, and we prove some upper and lower bounds for the positive equality-free fragment, $\mathcal{L} = \{\exists,\forall,\land,\lor\}$. The partial results are sufficient, e.g., for all extensions of the latter fragment.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
