COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Model Checking for Modal Intuitionistic Dependence Logic

## Model Checking for Modal Intuitionistic Dependence LogicAdd 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. |
## Other listsTesting & Verification For Computational Science Queens' Arts Seminar One Day Meeting - 5th Annual Symposium of the Cambridge Computational Biology Institute## Other talksKnot Floer homology and algebraic methods Radiocarbon as a carbon cycle tracer in the 21st century THE MATHEMATICAL MAGIC OF MIXED REALITY A tale of sleepless flies and ninna nanna. How Drosophila changes what we know about sleep. Sneks long balus 'Politics in Uncertain Times: What will the world look like in 2050 and how do you know? Towards bulk extension of near-horizon geometries TBC Graph Legendrians and SL2 local systems Aspects of adaptive Galerkin FE for stochastic direct and inverse problems |