negalg.csr2014-final.pdf (486.95 kB)
0/0

Block products and nesting negations in FO2

Download (486.95 kB)
conference contribution
posted on 23.02.2018 by Lukas Fleischer, Manfred Kufleitner, Alexander Lauser
The alternation hierarchy in two-variable first-order logic FO 2 [∈ < ∈] over words was recently shown to be decidable by Kufleitner and Weil, and independently by Krebs and Straubing. In this paper we consider a similar hierarchy, reminiscent of the half levels of the dot-depth hierarchy or the Straubing-Thérien hierarchy. The fragment of FO 2 is defined by disallowing universal quantifiers and having at most m∈-∈1 nested negations. One can view as the formulas in FO 2 which have at most m blocks of quantifiers on every path of their parse tree, and the first block is existential. Thus, the m th level of the FO 2 -alternation hierarchy is the Boolean closure of. We give an effective characterization of, i.e., for every integer m one can decide whether a given regular language is definable by a two-variable first-order formula with negation nesting depth at most m. More precisely, for every m we give ω-terms U m and V m such that an FO 2 -definable language is in if and only if its ordered syntactic monoid satisfies the identity U m ∈V m. Among other techniques, the proof relies on an extension of block products to ordered monoids. © 2014 Springer International Publishing Switzerland.

Funding

F.L. and M.K. were supported by the German Research Foundation (DFG) under grant DI 435/5-1

History

School

  • Science

Department

  • Computer Science

Published in

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Volume

8476 LNCS

Pages

176 - 189

Citation

FLEISCHER, L., KUFLEITNER, M. and LAUSER, A., 2014. Block products and nesting negations in FO2. IN: Hirsch, E. ...et al. (eds.) Computer Science - Theory and Applications. 9th International Computer Science Symposium in Russia, (CSR 2014), Moscow, Russia, June 7-11, 2014, Proceedings. Chaim: Springer, pp. 176-189.

Publisher

© Springer

Version

AM (Accepted Manuscript)

Publisher statement

This work is made available according to the conditions of the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) licence. Full details of this licence are available at: https://creativecommons.org/licenses/by-nc-nd/4.0/

Publication date

2014

Notes

This is a pre-copyedited version of a contribution published in Hirsch, E. ...et al. (eds.) Computer Science - Theory and Applications. 9th International Computer Science Symposium in Russia, (CSR 2014), published by Springer International. The definitive authenticated version is available online via https://doi.org/10.1007/978-3-319-06686-8_14

ISBN

9783319066851

ISSN

0302-9743

eISSN

1611-3349

Book series

Lecture Notes in Computer Science;8476

Language

en

Exports

Logo branding

Keyword(s)

Exports