-
- LUTZ Schröder
- DFKI Bremen and Universität Bremen, Bremen, Germany
-
- Dirk Pattinson
- Imperial College London, London, UK
説明
<jats:p> 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, in <jats:italic>PSPACE</jats:italic> . This leads to a unified derivation of tight <jats:italic>PSPACE</jats:italic> -bounds for a number of logics, including <jats:italic>K</jats:italic> , <jats:italic>KD</jats:italic> , 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. </jats:p>
収録刊行物
-
- ACM Transactions on Computational Logic
-
ACM Transactions on Computational Logic 10 (2), 1-33, 2009-02
Association for Computing Machinery (ACM)