Tractability Frontier of Data Complexity in Team Semantics

TL;DR

This paper investigates the computational complexity of model-checking in team semantics logics, identifying clear boundaries between tractable and intractable cases, and providing new reductions for inclusion logic.

Contribution

It delineates the data complexity frontiers for dependence, inclusion, and independence logics under team semantics, and offers a novel reduction for inclusion logic's model-checking problem.

Findings

Model-checking complexity frontiers are established for various team semantics logics.

Inclusion logic under lax semantics reduces to dual-Horn Boolean satisfiability, confirming PTIME complexity.

Clear distinctions between tractable and intractable cases are identified for different logic fragments.

Abstract

We study the data complexity of model-checking for logics with team semantics. We focus on dependence, inclusion, and independence logic formulas under both strict and lax team semantics. Our results delineate a clear tractability/intractability frontiers in data complexity of both quantifier-free and quantified formulas for each of the logics. For inclusion logic under the lax semantics, we reduce the model-checking problem to the satisfiability problem of so-called dual-Horn Boolean formulas. Via this reduction, we give an alternative proof for the known result that the data complexity of inclusion logic is in PTIME.