2026-07-20T05:06:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6579 2024-03-06T10:38:45Z ddc:004 open_access

Quine's Fluted Fragment is Non-Elementary Pratt-Hartmann, Ian Szwast, Wieslaw Tendera, Lidia Quine fluted fragment Purdy non-elementary satisfiability decidability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ian Pratt-Hartmann and Wieslaw Szwast and Lidia Tendera 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.39 urn:nbn:de:0030-drops-65791 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.39 eng https://creativecommons.org/licenses/by/3.0/legalcode