Combining DL-Lite_{bool}^N with Branching Time: A gentle Marriage

Combining DL-Lite_{bool}^N with Branching Time: A gentle Marriage

Víctor Gutiérrez-Basulto, Jean Christoph Jung

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

We study combinations of the description logic DL-Lite_{bool}^N with the branching temporal logics CTL* and CTL. We analyse two types of combinations, both with rigid roles: (i) temporal operators are applied to concepts and to ABox assertions, and (ii) temporal operators are applied to concepts and Boolean combinations of concept inclusions and ABox assertions. For the resulting logics, we present algorithms for the satisfiability problem and (mostly tight) complexity bounds ranging from ExpTime to 3ExpTime.
Keywords:
Knowledge Representation, Reasoning, and Logic: Computational Complexity of Reasoning
Knowledge Representation, Reasoning, and Logic: Description Logics and Ontologies
Knowledge Representation, Reasoning, and Logic: Geometric, Spatial, and Temporal Reasoning
Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation