Complexity Results in Team Semantics: Nonemptiness Is Not So Complex
Aleksi Anttila, Juha Kontinen, Fan Yang
TL;DR
This paper analyzes the complexity of the propositional logic with the nonemptiness atom, $PL(\textsc{ne})$, under team semantics. By exploiting convexity and union-closure properties, it proves that $\mathrm{MC}$ for $PL(\textsc{ne})$ lies in $P$, while $\mathrm{SAT}$ is $NP$-complete and $\mathrm{VAL}$ is $coNP$-complete, with precise reductions and small-model arguments. The work provides a tight complexity classification for SAT, VAL, and MC, and connects these results to broader frameworks such as BSML and modal extensions, highlighting the role of convexity in tractability. Overall, adding the nonemptiness atom to classical propositional logic does not increase SAT or VAL complexity, and the results offer a foundation for studying entailment and extensions to other convex logics.
Abstract
We initiate the study of the complexity-theoretic properties of convex logics in team semantics. We focus on the extension of classical propositional logic with the nonemptiness atom NE, a logic known to be both convex and union closed. We show that the satisfiability problem for this logic is NP-complete, that its validity problem is coNP-complete, and that its model-checking problem is in P.