Abstract
Modal description logics feature modalities that capture dependence of knowledge on parameters such
as time, place, or the information state of agents.
E.g., the logic S5ALC combines the standard description logic ALC with an S5-modality that can
be understood as an epistemic operator or as representing (undirected) change. This logic embeds into
a corresponding modal first-order logic S5FOL. We
prove a modal characterization theorem for this embedding, in analogy to results by van Benthem and
Rosen relating ALC to standard first-order logic:
We show that S5ALC with only local roles is, both
over finite and over unrestricted models, precisely
the bisimulation-invariant fragment of S5FOL, thus
giving an exact description of the expressive power
of S5ALC with only local roles