One quantifier alternation in first-order logic with modular predicates
One quantifier alternation in first-order logic with modular predicates
复制标题
具有模块化谓词的一阶逻辑中的一个量词交替
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Tobias Walter
中科院分区：
文献类型：
--
作者：
Manfred Kufleitner;Tobias Walter
添加模块谓词会产生一阶逻辑FO对单词的推广。Barrington，Compton，Strauping和Therien已经研究了具有序比较$x<；y$的FO[<；，mod]和关于$x等价的n$谓词的表达能力。FO[<；，MOD]-碎片的研究是由Chaubard，Pin和Strauping开创的。最近，Dartois和Paperman证明了双变量片段FO2[<；，mod]中的可定义性是可判定的。在本文中，我们将继续这一工作。
我们给出了Sigma2[<；，MOD]中字语言的一个有效的代数刻画。片段Sigma2由一阶公式组成，其形式为Penex范式，具有两个量词块，从一个存在块开始。此外，我们还证明了Sigma2[<；，mod]的最大子类Delta2[<；，mod]具有与二元逻辑FO2[<；，mod]相同的表达能力。这将Therien和Wilke的结果FO2[<；]=Delta2[<；]推广到模谓词。作为副产品，我们得到了FO2[<；，mod]的另一个可判定的刻划。
Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x equiv i mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in the two-variable fragment FO2[<,MOD] is decidable. In this paper we continue this line of work.
We give an effective algebraic characterization of the word languages in Sigma2[<,MOD]. The fragment Sigma2 consists of first-order formulas in prenex normal form with two blocks of quantifiers starting with an existential block. In addition we show that Delta2[<,MOD], the largest subclass of Sigma2[<,MOD] which is closed under negation, has the same expressive power as two-variable logic FO2[<,MOD]. This generalizes the result FO2[<] = Delta2[<] of Therien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of FO2[<,MOD].