Complexity of Modal Logics of Relations
Maarten Marx
Abstract:
We consider two families of modal logics of relations: arrow logic and
cylindric modal logic and several natural expansions of these, interpreted
on a range of (relativised) modelclasses. We give a systematic study
of the complexity of the validity problem of these logics, obtaining
price tags for various features as assumptions on the universe of the
models, similarity types, and number of variables involved. The general
picture is that the process of relativisation turns an undecidable logic
into one whose validity problem is exptimecomplete. There
are interesting deviations to this though, which we also discuss. The
numerous results in this paper are all directed to obtain a better
understanding why relativisation can turn an undecidable modal logic
of relations into a decidable one. We connect the semantic way of
``taming logic'' by relativisation with the syntactic approach of
isolating decidable socalled guarded fragments by showing that validity
of loosely guarded formulas is preserved under relativisation.