LIPIcs.CSL.2016.39.pdf
- Filesize: 0.55 MB
- 21 pages
Document
Quine's Fluted Fragment is Non-Elementary
Authors
-
Part of:
Volume:
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-08-29
Cite As Get BibTex
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)
https://doi.org/10.4230/LIPIcs.CSL.2016.39
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.
Subject Classification
Keywords
- Quine
- fluted fragment
- Purdy
- non-elementary
- satisfiability
- decidability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998.
-
E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997.
-
E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997.
-
U. Hustadt, R. Schmidt, and L. Georgieva. A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science, 1(3):251-276, 2004.
-
C. Lutz and U. Sattler. The complexity of reasoning with Boolean modal logics. In F. Wolter, H. Wansing, M. de Rijke, and M. Zakharyaschev, editors, Advances in Modal Logic, volume 3, pages 1-20, Menlo Park, 2001. CLSI Publications.
-
A. Noah. Predicate-functors and the limits of decidability in logic. Notre Dame Journal of Formal Logic, 21(4):701-707, 1980.
-
W. C. Purdy. Decidability of fluted logic with indentity. Notre Dame Journal of Formal Logic, 37(1):84-104, 1996.
-
W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 61(2):608-620, 1996.
-
W. C. Purdy. Quine’s limits of decision. Journal of Symbolic Logic, 64(4):1439-1466, 1999.
-
W. C. Purdy. Complexity and nicety of fluted logic. Studia Logica, 71:177-198, 2002.
-
W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62. University of Vienna, 1969.
-
W. V. Quine. Algebraic logic and predicate functors. In The Ways of Paradox, pages 283-307. Harvard University Press, revised and enlarged edition, 1976.
-
W. V. Quine. The variable. In The Ways of Paradox, pages 272-282. Harvard University Press, revised and enlarged edition, 1976.
-
V. Rantala. Constituents. In R. Bogdan, editor, Jaakko Hintikka, volume 8 of Profiles, pages 43-76. Springer Netherlands, 1987.
-
R. Schmidt and U. Hustadt. A resolution decision procedure for fluted logic. In D. McAllester, editor, Proceedings, CADE, number 1831 in LNAI, pages 433-448. Springer-Verlag, 2000.