Two-variable first order logic with modular predicates is decidable over words

Prelegent(ci)

Charles Paperman

Afiliacja

LIAFA, University Paris-Diderot

Termin

7 listopada 2012 14:15

Pokój

p. 5870

Tytuł w języku angielskim

joint work with Luc Dartois

Seminarium

Seminarium „Teoria automatów”

---

We consider first order formulae over the signature consisting of the symbols of the alphabet, the symbol $<$ (interpreted as a linear order) and the set $\MOD$ of modular numerical predicates. We study the expressive power of $\FO2[<,MOD]$, the two-variable first order logic over this signature, interpreted over finite words. We give an algebraic characterization of the corresponding regular languages in terms of their syntactic morphisms. It follows that one can decide whether a given regular language is captured by $\FO2[<,MOD]$. Our proofs rely on a combination of arguments from semigroup theory (stamps), model theory (E-F games) and combinatorics.

---