Algebraic Characterization of the Alternation Hierarchy in FO^2[<] on Finite Words
Howard Straubing · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2011
We give an algebraic characterization of the quantifier alternation hierarchy in first-order two-variable logic on finite words. As a result, we obtain a new proof that this hierarchy is strict. We also show that the first two levels of the hierarchy have decidable membership problems, and conjecture an algebraic decision procedure for the other levels.