Model Checking for Modal Intuitionistic Dependence Logic

Add to your list(s) Download to your calendar using vCal

• Yang, F (University of Helsinki)
• Monday 26 March 2012, 16:00-16:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact Mustapha Amrani.

Semantics and Syntax: A Legacy of Alan Turing

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.