Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.39
URN: urn:nbn:de:0030-drops-65791
URL: https://drops.dagstuhl.de/opus/volltexte/2016/6579/
Pratt-Hartmann, Ian ; Szwast, Wieslaw ; Tendera, Lidia
Quine's Fluted Fragment is Non-Elementary
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{pratthartmann_et_al:LIPIcs:2016:6579,
author = {Ian Pratt-Hartmann and Wieslaw Szwast and Lidia Tendera},
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 = {Jean-Marc Talbot and Laurent Regnier},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6579},
URN = {urn:nbn:de:0030-drops-65791},
doi = {10.4230/LIPIcs.CSL.2016.39},
annote = {Keywords: Quine, fluted fragment, Purdy, non-elementary, satisfiability, decidability}
}
| Keywords: | Quine, fluted fragment, Purdy, non-elementary, satisfiability, decidability | |
| Seminar: | 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 29.08.2016 |
