2026-07-22T08:34:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4836 2024-03-06T10:35:24Z ddc:004 open_access

Parameterized Complexity of Fixed Variable Logics Berkholz, Christoph Elberfeld, Michael Parameterized complexity polynomial space first-order logic pebble games regular resolutions We study the complexity of model checking formulas in first-order logic parameterized by the number of distinct variables in the formula. This problem, which is not known to be fixed-parameter tractable, resisted to be properly classified in the context of parameterized complexity. We show that it is complete for a newly-defined complexity class that we propose as an analog of the classical class PSPACE in parameterized complexity. We support this intuition by the following findings: First, the proposed class admits a definition in terms of alternating Turing machines in a similar way as PSPACE can be defined in terms of polynomial-time alternating machines. Second, we show that parameterized versions of other PSPACE-complete problems, like winning certain pebble games and finding restricted resolution refutations, are complete for this class. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Berkholz and Michael Elberfeld 2014 Is Part Of LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2014.109 urn:nbn:de:0030-drops-48367 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.109 eng https://creativecommons.org/licenses/by/3.0/legalcode