The Fluted Fragment Revisited

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

Research output: Contribution to journalArticlepeer-review

286 Downloads (Pure)

Abstract

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originating in the work of 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 FLm, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all m ≥ 1. We show that, for m ≥ 2, this sub-fragment forces m/2-tuply exponentially large models, and that its satisfiability problem is m/2-NExpTime-hard. We further establish that, for m ≥ 3, any satisfiable FLm-formula has a model of at most (m-2)-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in (m-2)-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for FLm for all m ≤4.
Original languageEnglish
Pages (from-to)1020-1048
Number of pages29
JournalThe Journal of Symbolic Logic
Volume84
Issue number3
Early online date6 Jun 2019
DOIs
Publication statusPublished - 16 Sept 2019

Keywords

  • satisfiability
  • complexity
  • first-order logic
  • fluted fragment

Fingerprint

Dive into the research topics of 'The Fluted Fragment Revisited'. Together they form a unique fingerprint.

Cite this