Quine's Fluted Fragment is Non-Elementary
CSL, pp. 39:1-39:21, 2016.
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 consi...More
Full Text (Upload PDF)
PPT (Upload PPT)