Quine's Fluted Fragment
From International Center for Computational Logic
Quine's Fluted Fragment
Talk by Ian Pratt-Hartmann
- Start: 9. May 2019 at 1:00 pm
- End: 9. May 2019 at 2:30 pm
- Research group: Computational Logic
- Event series: KBS Seminar
- iCal
We consider the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified in 1968 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 the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all non-negative m. We obtain upper and lower complexity bounds for this fragment that coincide for all m up to the value 4.