2026-07-23T04:09:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3943 2024-03-06T10:34:40Z ddc:004 open_access

Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable Kufleitner, Manfred Lauser, Alexander automata theory semigroups regular languages first-order logic 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 for a given regular language and a non-negative integer~$m$ it is decidable 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] quantifier alternation hierarchy. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Kufleitner and Alexander Lauser 2013 Is Part Of LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2013.305 urn:nbn:de:0030-drops-39438 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.305 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode