文章基本信息

标题：Quine's Fluted Fragment is Non-Elementary
本地全文：下载
作者：Ian Pratt-Hartmann ; Wieslaw Szwast ; Lidia Tendera 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：62
页码：39:1-39:21
DOI：10.4230/LIPIcs.CSL.2016.39
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Quine; fluted fragment; Purdy; non-elementary; satisfiability; decidability