Tractability Frontier of Data Complexity in Team Semantics
Logic in Computer Science
2021-08-16 v3
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.
Keywords
Cite
@article{arxiv.1503.01144,
title = {Tractability Frontier of Data Complexity in Team Semantics},
author = {Arnaud Durand and Juha Kontinen and Nicolas de Rugy-Altherre and Jouko Väänänen},
journal= {arXiv preprint arXiv:1503.01144},
year = {2021}
}