Advertisement
Published in:
2013 | OriginalPaper | Chapter
Model Checking for Modal Intuitionistic Dependence Logic
Authors : Johannes Ebbing, Peter Lohmann, Fan Yang
Published in: Logic, Language, and Computation
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Modal intuitionistic dependence logic (
$\mathcal MIDL $
) incorporates the notion of “dependence” between propositions into the usual modal logic and has connectives which correspond to intuitionistic connectives in a certain sense. It is the modal version of a variant of first-order dependence logic (Väänänen 2007) considered by Abramsky and Väänänen (2009) basing on Hodges’
team semantics
(1997).
In this paper, we study the computational complexity of the model checking problem for
$\mathcal MIDL$
and its fragments built by restricting the operators allowed in the logics. In particular, we show that the model checking problem for
$\mathcal MIDL$
in general is
PSPACE
-complete and that for propositional intuitionistic dependence logic is co
NP
-complete.