Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable
Logic in Computer Science
2013-01-01 v1 Formal Languages and Automata Theory
Abstract
We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with the FO^2[<,suc] alternation hierarchy.
Cite
@article{arxiv.1212.6500,
title = {Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable},
author = {Manfred Kufleitner and Alexander Lauser},
journal= {arXiv preprint arXiv:1212.6500},
year = {2013}
}
Comments
Accepted at STACS 2013