BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Model Checking for Modal Intuitionistic Dependence
Logic - Yang\, F (University of Helsinki)
DTSTART;TZID=Europe/London:20120326T160000
DTEND;TZID=Europe/London:20120326T163000
UID:TALK37092AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/37092
DESCRIPTION: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 Vnn
en (2007)\, as a new approach to independence-frie
ndly logic (Hintikka\, Sandu\, 1989). Sentences of
D have exactly the same expressive power as sente
nces of existential second-order logic (Vnnen 2007
\, c.f. Enderton\, 1970 and Walkoe\, 1970). The co
mpositional semantics of D is team semantics\, ori
ginally developed by Hodges (1997) for independenc
e-friendly logic. Abramsky and Vnnen (2009) studie
d Hodges construction in a more general context an
d introduced BID-logic\, which extends dependence
and includes intuitionistic implication\, Boolean
disjunction\, as well as linear implication. It wa
s shown that the intuitionistic fragment of BID-lo
gic\, called intuitionistic dependence logic\, has
exactly the same expressive power as the full sec
ond-order logic\, on the level of sentences (Yang\
, 2010). \n\nThe modal version of D\, modal depend
ence logic (MDL) was defined by Vnnen (2008). A na
tural variant of MDL is modal intuitionistic depen
dence logic\, where the intuitionistic implication
and Boolean disjunction are added into the settin
g. In this paper we show that the model checking p
roblem for MIDL in general is PSPACE-complete. Fur
thermore\, we consider fragments of MIDL built by
restricting the operators allowed in the logic. It
turns out that apart from known NP-complete as we
ll as tractable fragments there also are some coNP
-complete fragments\, e.g. propositional intuition
istic dependence logic.\n\n
LOCATION:Seminar Room 1\, Newton Institute
CONTACT:Mustapha Amrani
END:VEVENT
END:VCALENDAR