DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2016.39

Quine's Fluted Fragment is Non-Elementary

Authors: Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.

Cite as

Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. Quine's Fluted Fragment is Non-Elementary. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{pratthartmann_et_al:LIPIcs.CSL.2016.39,
  author =	{Pratt-Hartmann, Ian and Szwast, Wieslaw and Tendera, Lidia},
  title =	{{Quine's Fluted Fragment is Non-Elementary}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.39},
  URN =		{urn:nbn:de:0030-drops-65791},
  doi =		{10.4230/LIPIcs.CSL.2016.39},
  annote =	{Keywords: Quine, fluted fragment, Purdy, non-elementary, satisfiability, decidability}
}

Document

DOI: 10.4230/LIPIcs.STACS.2013.317

FO^2 with one transitive relation is decidable

Authors: Wieslaw Szwast and Lidia Tendera

Published in: LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)

Abstract

We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.

Cite as

Wieslaw Szwast and Lidia Tendera. FO^2 with one transitive relation is decidable. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 317-328, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{szwast_et_al:LIPIcs.STACS.2013.317,
  author =	{Szwast, Wieslaw and Tendera, Lidia},
  title =	{{FO^2 with one transitive relation is decidable}},
  booktitle =	{30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)},
  pages =	{317--328},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-50-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{20},
  editor =	{Portier, Natacha and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.317},
  URN =		{urn:nbn:de:0030-drops-39449},
  doi =		{10.4230/LIPIcs.STACS.2013.317},
  annote =	{Keywords: classical decision problem, two-variable first-order logic, decidability, computational complexity}
}

Search Results

Documents authored by Szwast, Wieslaw

Quine's Fluted Fragment is Non-Elementary

Abstract

Cite as

FO^2 with one transitive relation is decidable

Abstract

Cite as

Thanks for your feedback!

Could not send message