PSPACE bounds for rank-1 modal logics
PSPACE bounds for rank-1 modal logics
复制标题
1 阶模态逻辑的 PSPACE 界限
DOI：
10.1145/1462179.1462185
复制
发表时间：
2009
影响因子：
0.5
通讯作者：
Schröder L
中科院分区：
文献类型：
--
作者：
Schröder L
由于缺乏适用于各种逻辑的通用算法方法，为给定的模态逻辑建立复杂性界限通常是一项艰巨的任务。目前的工作是一个一般理论的复杂性模态逻辑的一步。我们的主要结果是，所有秩1逻辑享有浅模型属性，因此，在温和的假设下，其axiomatisation的格式，在PSPACE。这导致了一个统一的推导紧PSPACE界限的一些逻辑，包括K，KD，联盟逻辑，分级模态逻辑，多数逻辑，概率模态逻辑。此外，我们的通用算法发现，见证愉快的证明理论的性质，包括一个弱子公式属性的Tableau证明。这种普遍性是由一个coalgebraic语义，方便地抽象的细节，一个给定的模型类，从而允许覆盖范围广泛的逻辑在一个统一的方式。
For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, inPSPACE. This leads to a unified derivation of tightPSPACE-bounds for a number of logics, includingK,KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.