带一阶前趋分离逻辑的复杂性
The Complexity of Prenex Separation Logic with One Selector
摘要：
我们首先证明了具有$k\geq1$选择器域的分离逻辑（$\seplogk{k}$）的所有前向列公式的无限可满足性都可以化为有限可满足性。第二，我们表明，这需要的可判定性的有限和无限的可满足性问题的类前向公式的$\seplogk{1}$，减少到一阶理论的一元函数符号和一元谓词符号。我们还证明了复杂性不是初等的，通过减少从一元函数符号的一阶理论。最后证明了$\exists^*\forall^*$语言中带量词前缀的前趋$\seplogk{1}$公式的Bernays-Schönfinkel-Ramsey片段是\pspace -完全的.一个完整的（层次）分类的复杂性前束$\seplogk{1}$的定义，根据量词交替深度是一个悬而未决的问题。
英文摘要：
We first show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with $k\geq1$ selector fields ($\seplogk{k}$). Second, we show that this entails the decidability of the finite and infinite satisfiability problem for the class of prenex formulas of $\seplogk{1}$, by reduction to the first-order theory of one unary function symbol and unary predicate symbols. We also prove that the complexity is not elementary, by reduction from the first-order theory of one unary function symbol. Finally, we prove that the Bernays-Schönfinkel-Ramsey fragment of prenex $\seplogk{1}$ formulae with quantifier prefix in the language $\exists^*\forall^*$ is \pspace-complete. The definition of a complete (hierarchical) classification of the complexity of prenex $\seplogk{1}$, according to the quantifier alternation depth is left as an open problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
