A Characterization Theorem for a Modal Description Logic

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 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.

Cite

Text

Wild and Schröder. "A Characterization Theorem for a Modal Description Logic." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/181

Markdown

[Wild and Schröder. "A Characterization Theorem for a Modal Description Logic." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/wild2017ijcai-characterization/) doi:10.24963/IJCAI.2017/181

BibTeX

@inproceedings{wild2017ijcai-characterization,
  title     = {{A Characterization Theorem for a Modal Description Logic}},
  author    = {Wild, Paul and Schröder, Lutz},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2017},
  pages     = {1304-1310},
  doi       = {10.24963/IJCAI.2017/181},
  url       = {https://mlanthology.org/ijcai/2017/wild2017ijcai-characterization/}
}