LIPIcs.STACS.2013.305.pdf
- Filesize: 0.53 MB
- 12 pages
Document
Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable
Authors
-
Part of:
Volume:
30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution-NoDerivs 3.0 Unported license
- Publication Date: 2013-02-26
Cite AsGet BibTex
Manfred Kufleitner and Alexander Lauser. Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 305-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.STACS.2013.305
https://doi.org/10.4230/LIPIcs.STACS.2013.305
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 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.
Keywords
- automata theory
- semigroups
- regular languages
- first-order logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads