One quantifier alternation in first-order logic with modular predicates

Kufleitner, Manfred; Walter, Tobias

doi:10.1051/ita/2014024

Kufleitner, Manfred ¹ ; Walter, Tobias ¹

¹ University of Stuttgart, FMI, Germany.

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 1, pp. 1-22

Voir la notice de l'article provenant de la source Numdam

Résumé

Adding modular predicates yields a generalization of first-order logic $F O$ over words. The expressive power of $F O [<, M O D]$ with order comparison $x < y$ and predicates for $x \equiv i m o d n$ has been investigated by Barrington et al. The study of $F O [<, M O D]$ -fragments was initiated by Chaubard et al. More recently, Dartois and Paperman showed that definability in the two-variable fragment $F O^{2} [<, M O D]$ is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in $Σ_{2} [<, M O D]$ . The fragment $Σ_{2}$ consists of first-order formulas in prenex normal form with two blocks of quantifiers starting with an existential block. In addition we show that $Δ_{2} [<, M O D]$ , the largest subclass of $Σ_{2} [<, M O D]$ which is closed under negation, has the same expressive power as two-variable logic $F O^{2} [<, M O D]$ . This generalizes the result $F O^{2} [<] = Δ_{2} [<]$ of Thérien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of $F O^{2} [<, M O D]$ .

Reçu le : 2013-10-17
Accepté le : 2014-06-18

MR Zbl

DOI : 10.1051/ita/2014024

Classification : 68Q70, 03D05, 20M35, 68Q45
Keywords: Finite monoid, syntactic homomorphism, logical fragment, first-order logic, modular predicate

Affiliations des auteurs :

Kufleitner, Manfred ¹ ; Walter, Tobias ¹

¹ University of Stuttgart, FMI, Germany.

@article{ITA_2015__49_1_1_0,
     author = {Kufleitner, Manfred and Walter, Tobias},
     title = {One quantifier alternation in first-order logic with modular predicates},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {1--22},
     publisher = {EDP-Sciences},
     volume = {49},
     number = {1},
     year = {2015},
     doi = {10.1051/ita/2014024},
     mrnumber = {3342170},
     zbl = {1339.03014},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2014024/}
}

TY  - JOUR
AU  - Kufleitner, Manfred
AU  - Walter, Tobias
TI  - One quantifier alternation in first-order logic with modular predicates
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2015
SP  - 1
EP  - 22
VL  - 49
IS  - 1
PB  - EDP-Sciences
UR  - http://geodesic.mathdoc.fr/articles/10.1051/ita/2014024/
DO  - 10.1051/ita/2014024
LA  - en
ID  - ITA_2015__49_1_1_0
ER  -

%0 Journal Article
%A Kufleitner, Manfred
%A Walter, Tobias
%T One quantifier alternation in first-order logic with modular predicates
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2015
%P 1-22
%V 49
%N 1
%I EDP-Sciences
%U http://geodesic.mathdoc.fr/articles/10.1051/ita/2014024/
%R 10.1051/ita/2014024
%G en
%F ITA_2015__49_1_1_0

Kufleitner, Manfred; Walter, Tobias. One quantifier alternation in first-order logic with modular predicates. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 1, pp. 1-22. doi: 10.1051/ita/2014024

Cité par Sources :

Parcourir par

Geodesic

Parcourir par