On the Complexity of Modal Team Logic and Two-Variable Team Logic.
Martin Lück · arXiv (Cornell University) · 2017
We study modal team logic MTL and the dependence-free fragment FO^2[~] of two-variable team logic, which extend modal logic ML and two-variable logic FO^2 with team semantics by a Boolean negation ~. We settle the open question of the complexity of their respective satisfiability problems, and prove that both are complete for a non-elementary complexity class. We also prove that the model checking problem is PSPACE-complete for several fragments of MTL and FO[~]. Based on the well-known standard translation from ML to FO^2, we propose an team-semantical translation from MTL into FO^2[~].