DROPS

Document

Structure Theorem and Strict Alternation Hierarchy for FOÃ‚Â² on Words

Authors: Philipp Weis and Neil Immerman

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)

Abstract

It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and well-studied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to FO$^2[<]$ and FO$^2[<,suc]$, the latter of which includes the binary successor relation in addition to the linear ordering on string positions. For both languages, our structure theorems show exactly what is expressible using a given quantifier depth, $n$, and using $m$ blocks of alternating quantifiers, for any $mleq n$. Using these characterizations, we prove, among other results, that there is a strict hierarchy of alternating quantifiers for both languages. The question whether there was such a hierarchy had been completely open since it was asked in [Etessami, Vardi, and Wilke 1997].

Cite as

Philipp Weis and Neil Immerman. Structure Theorem and Strict Alternation Hierarchy for FOÃ‚Â² on Words. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{weis_et_al:DagSemProc.06451.6,
  author =	{Weis, Philipp and Immerman, Neil},
  title =	{{Structure Theorem and Strict Alternation Hierarchy for FO\~{A}‚\^{A}² on Words}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.6},
  URN =		{urn:nbn:de:0030-drops-9751},
  doi =		{10.4230/DagSemProc.06451.6},
  annote =	{Keywords: Descriptive complexity, finite model theory, alternation hierarchy, Ehrenfeucht-Fraisse games}
}

Search Results

Documents authored by Weis, Philipp

Structure Theorem and Strict Alternation Hierarchy for FOÃ‚Â² on Words

Abstract

Cite as

Thanks for your feedback!

Could not send message