Quine’s Fluted Fragment is Non-elementary

Ian Pratt-Hartmann, Wiesław Szwast , Lidia Tendera

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    95 Downloads (Pure)

    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 subfragment 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.
    Original languageEnglish
    Title of host publication25th EACSL Annual Conference on Computer Science Logic
    EditorsLaurent Regnier, Jean-Marc Talbot
    DOIs
    Publication statusPublished - 13 Jun 2016

    Publication series

    Name25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
    PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    ISSN (Electronic)1868-8969

    Fingerprint

    Dive into the research topics of 'Quine’s Fluted Fragment is Non-elementary'. Together they form a unique fingerprint.

    Cite this