2017/05/17 by Wild, Paul, Schröder, Lutz
#03B10 #03B42 #03B45 #03B70 #03C80 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.4 #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1705.06214
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 S5-ALC 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 S5-FOL. 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 S5-ALC with only local roles is, both over finite and over unrestricted models, precisely the bisimulation invariant fragment of S5-FOL, thus giving an exact description of the expressive power of S5-ALC with only local roles.