Search Results

Documents authored by Immerman, Neil

Document
DOI: 10.4230/LIPIcs.MFCS.2024.34
On the Number of Quantifiers Needed to Define Boolean Functions

Authors: Marco Carmosino, Ronald Fagin, Neil Immerman, Phokion G. Kolaitis, Jonathan Lenchner, and Rik Sengupta

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
The number of quantifiers needed to express first-order (FO) properties is captured by two-player combinatorial games called multi-structural games. We analyze these games on binary strings with an ordering relation, using a technique we call parallel play, which significantly reduces the number of quantifiers needed in many cases. Ordered structures such as strings have historically been notoriously difficult to analyze in the context of these and similar games. Nevertheless, in this paper, we provide essentially tight bounds on the number of quantifiers needed to characterize different-sized subsets of strings. The results immediately give bounds on the number of quantifiers necessary to define several different classes of Boolean functions. One of our results is analogous to Lupanov’s upper bounds on circuit size and formula size in propositional logic: we show that every Boolean function on n-bit inputs can be defined by a FO sentence having (1+ε)n/log(n) + O(1) quantifiers, and that this is essentially tight. We reduce this number to (1 + ε)log(n) + O(1) when the Boolean function in question is sparse.
Cite as

Marco Carmosino, Ronald Fagin, Neil Immerman, Phokion G. Kolaitis, Jonathan Lenchner, and Rik Sengupta. On the Number of Quantifiers Needed to Define Boolean Functions. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 34:1-34:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{carmosino_et_al:LIPIcs.MFCS.2024.34,
  author =	{Carmosino, Marco and Fagin, Ronald and Immerman, Neil and Kolaitis, Phokion G. and Lenchner, Jonathan and Sengupta, Rik},
  title =	{{On the Number of Quantifiers Needed to Define Boolean Functions}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{34:1--34:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.34},
  URN =		{urn:nbn:de:0030-drops-205907},
  doi =		{10.4230/LIPIcs.MFCS.2024.34},
  annote =	{Keywords: logic, combinatorial games, Boolean functions, quantifier number}
}
Document
DOI: 10.4230/DagSemProc.06451.6
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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact