Why are many-dimensional modal logics so robustly undecidable?
One of the main reasons for the success of modal logic in computer science is their unusual robust decidability. For example,
standard modal logics such as epistemic logics, propositional dynamic logic, or standard temporal logics are decidable in
ExpTime. This situation changes drastically as soon as combined modal logics such as temporal epistemic logics, spatio-temporal
logics, or first-order modal and temporal logics are considered. Indeed, straightforward constructions of combined modal logics
from simple modal logics almost certainly result in undecidable or even highly undecidable systems. The aim of this talk is
twofold: (i) to discuss explanations for this phenomenon and (ii) to use the insights gained from this discussion to provide
methodologies for constructing computationally well-behaved combined modal logics.
Bio: Frank Wolter is a Professor
in the Department of Computer Science at the University of Liverpool. He is working in Knowledge Representation and Reasoning
(Description Logic, Spatial Logic) and Modal and Temporal Logic. He is co-editor of the Handbook of Modal Logic, published
by Elsevier in 2007.