On the Complexity of Team Logic and its Two-Variable Fragment
Martin L\"uck

TL;DR
This paper investigates the computational complexity of team logic FO(~) and its two-variable fragment FO2(~), establishing decidability, complexity classifications, and translations to other logical frameworks.
Contribution
It proves that FO2(~) satisfiability is complete for TOWER(poly) and classifies model checking complexity, extending modal logic translations to team semantics.
Findings
FO2(~) satisfiability is decidable and TOWER(poly)-complete.
Model checking exhibits a dichotomy between PSPACE and ATIME-ALT(exp, poly).
Translation methods connect modal team logic to FO2(~) and second-order logic.
Abstract
We study the logic FO(~), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown axiomatizable, but otherwise has not yet received much attention in questions of computational complexity. In this paper, we consider its two-variable fragment FO2(~) and prove that its satisfiability problem is decidable, and in fact complete for the recently introduced non-elementary class TOWER(poly). Moreover, we classify the complexity of model checking of FO(~) with respect to the number of variables and the quantifier rank, and prove a dichotomy between PSPACE- and ATIME-ALT(exp, poly)-completeness. To achieve the lower bounds, we propose a translation from modal team logic MTL to FO2(~) that extends the well-known standard translation from modal logic ML to FO2. For the upper bounds, we translate to a fragment of second-order logic.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
