Tractability Frontier of Data Complexity in Team Semantics

Arnaud Durand
Juha Kontinen
Nicolas de Rugy-Altherre
Jouko Väänänen

We study the data complexity of model-checking for logics with team semantics. For dependence and independence logic, we completely characterize the tractability/intractability frontier of data complexity of both quantifier-free and quantified formulas. For inclusion logic formulas, we reduce the model-checking problem to the satisfiability problem of so-called Dual-Horn propositional formulas. Via this reduction, we give an alternative proof for the recent result showing that the data complexity of inclusion logic is in PTIME.

In Javier Esparza and Enrico Tronci: Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), Genoa, Italy, 21-22nd September 2015, Electronic Proceedings in Theoretical Computer Science 193, pp. 73–85.
Published: 23rd September 2015.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: