Computational Aspects of Logics in Team Semantics (Tutorial)

Team Semantics is a logical framework for the study of various dependency notions that are important in many areas of science. The starting point of this research is marked by the publication of the monograph Dependence Logic (Jouko Väänänen, 2007) in which first-order dependence logic is developed and studied. Since then team semantics has evolved into a flexible framework in which numerous logics have been studied. Much of the work in team semantics has so far focused on results concerning either axiomatic characterizations or the expressive power and computational aspects of various logics. This tutorial provides an introduction to team semantics with a focus on results regarding expressivity and computational aspects of the most prominent logics of the area. In particular, we discuss dependence, independence and inclusion logics in first-order, propositional, and modal team semantics. We show that first-order dependence and independence logic are equivalent with existential second-order logic and inclusion logic with greatest fixed point logic. In the propositional and modal settings we characterize the expressive power of these logics by so-called team bisimulations and determine the complexity of their model checking and satisfiability problems.