Abstract

In this paper we consider the complexity of model checking for modal intuitionistic dependence logic (MIDL). MIDL is a natural variant of first-order dependence logic (D), which was introduced by Vnnen (2007), as a new approach to independence-friendly logic (Hintikka, Sandu, 1989). Sentences of D have exactly the same expressive power as sentences of existential second-order logic (Vnnen 2007, c.f. Enderton, 1970 and Walkoe, 1970). The compositional semantics of D is team semantics, originally developed by Hodges (1997) for independence-friendly logic. Abramsky and Vnnen (2009) studied Hodges construction in a more general context and introduced BID -logic, which extends dependence and includes intuitionistic implication, Boolean disjunction, as well as linear implication. It was shown that the intuitionistic fragment of BID -logic, called intuitionistic dependence logic, has exactly the same expressive power as the full second-order logic, on the level of sentences (Yang, 2010).

The modal version of D, modal dependence logic (MDL) was defined by Vnnen (2008). A natural variant of MDL is modal intuitionistic dependence logic, where the intuitionistic implication and Boolean disjunction are added into the setting. In this paper we show that the model checking problem for MIDL in general is PSPACE -complete. Furthermore, we consider fragments of MIDL built by restricting the operators allowed in the logic. It turns out that apart from known NP-complete as well as tractable fragments there also are some coNP-complete fragments, e.g. propositional intuitionistic dependence logic.