一句话:系统刻画模态与命题依赖逻辑中有效性与蕴涵问题的复杂度,并证明模态依赖逻辑有效性为 NEXPTIME 完全。
模态与命题依赖逻辑的可满足性复杂度已有较系统的研究,例如 Sevenster 证明模态依赖逻辑可满足性为 NEXPTIME 完全;但其有效性与蕴涵性质此前基本未被讨论。本文在 team 语义框架下考察由标准模态逻辑和命题逻辑分别加入依赖、独立与包含等概念得到的一族逻辑,对这些逻辑的有效性与蕴涵问题给出较全面的复杂度分类。关键结果之一是把模态依赖逻辑的有效性问题确定为 NEXPTIME 完全,从而否定了此前认为该问题复杂度更高的猜想。
The computational properties of modal and propositional dependence logics have been extensively studied over the past few years, starting from a result by Sevenster showing NEXPTIME-completeness of the satisfiability problem for modal dependence logic. Thus far, however, the validity and entailment properties of these logics have remained mostly unaddressed. This paper provides a comprehensive classification of the complexity of validity and entailment in various modal and propositional dependence logics. The logics examined are obtained by extending the standard modal and propositional logics with notions of dependence, independence, and inclusion in the team semantics context. In particular, we address the question of the complexity of validity in modal dependence logic. By showing that it is NEXPTIME-complete we refute an earlier conjecture proposing a higher complexity for the problem.