ML Anthology

Combining DL-Lite_boolN with Branching Time: A Gentle Marriage

Víctor Gutiérrez-Basulto, Jean Christoph Jung
IJCAI 2017 pp. 1074-1080
doi:10.24963/IJCAI.2017/149 /ijcai/2017/gutierrezbasulto2017ijcai-combining/

Abstract

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.

PDF IJCAI Semantic Scholar

Cite

Text

Gutiérrez-Basulto and Jung. "Combining DL-Lite_boolN with Branching Time: A Gentle Marriage." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/149

Markdown

[Gutiérrez-Basulto and Jung. "Combining DL-Lite_boolN with Branching Time: A Gentle Marriage." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/gutierrezbasulto2017ijcai-combining/) doi:10.24963/IJCAI.2017/149

BibTeX

@inproceedings{gutierrezbasulto2017ijcai-combining,
  title     = {{Combining DL-Lite_boolN with Branching Time: A Gentle Marriage}},
  author    = {Gutiérrez-Basulto, Víctor and Jung, Jean Christoph},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2017},
  pages     = {1074-1080},
  doi       = {10.24963/IJCAI.2017/149},
  url       = {https://mlanthology.org/ijcai/2017/gutierrezbasulto2017ijcai-combining/}
}