A Characterization Theorem for a Modal Description Logic

A Characterization Theorem for a Modal Description Logic

Paul Wild, Lutz Schröder

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 1304-1310. https://doi.org/10.24963/ijcai.2017/181

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.
Keywords:
Knowledge Representation, Reasoning, and Logic: Description Logics and Ontologies
Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation
Knowledge Representation, Reasoning, and Logic: Reasoning about Knowlege and Belief