paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Validity and Entailment in Modal and Propositional Dependence Logics

模态与命题依赖逻辑中的有效性与蕴涵
LMCS vol.Volume 15, Issue 22019匹配度 1/10 · 该论文研究模态/命题依赖逻辑的有效性与蕴涵复杂度,属于纯逻辑与自动机理论,未涉及静态分析、程序验证、浮点程序分析、贝叶斯程序分析或 LLM/Agent 交叉。虽然形式化验证可能与逻辑相关,但距离用户当前研究画像的核心问题很远。引用 2 inbox
Miika Hannula
crossref: 2026-09-10

AI 速览

一句话:系统刻画模态与命题依赖逻辑中有效性与蕴涵问题的复杂度,并证明模态依赖逻辑有效性为 NEXPTIME 完全。

模态与命题依赖逻辑的可满足性复杂度已有较系统的研究,例如 Sevenster 证明模态依赖逻辑可满足性为 NEXPTIME 完全;但其有效性与蕴涵性质此前基本未被讨论。本文在 team 语义框架下考察由标准模态逻辑和命题逻辑分别加入依赖、独立与包含等概念得到的一族逻辑,对这些逻辑的有效性与蕴涵问题给出较全面的复杂度分类。关键结果之一是把模态依赖逻辑的有效性问题确定为 NEXPTIME 完全,从而否定了此前认为该问题复杂度更高的猜想。

问题
模态与命题依赖逻辑的有效性和蕴涵问题的计算复杂度此前缺乏系统研究,本文旨在对其进行完整分类。
方法
在 team 语义下,将标准模态逻辑和命题逻辑分别扩展以依赖、独立与包含等概念,并分析所得逻辑的有效性与蕴涵复杂度。
评估
通过复杂度分类与完全性证明给出结果,特别证明模态依赖逻辑有效性是 NEXPTIME 完全,并推翻此前关于更高复杂度的猜想。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot802,
  title = {Validity and Entailment in Modal and Propositional Dependence Logics},
  author = {Miika Hannula},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 2},
  year = {2019},
  doi = {10.23638/lmcs-15(2:4)2019}
}