Combining DL-LiteNbool with branching time: a gentle marriage

Gutierrez Basulto, Victor ORCID: https://orcid.org/0000-0002-6117-5459 and Jung, Jean Christoph 2017. Combining DL-LiteNbool with branching time: a gentle marriage. Presented at: 26th International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19-25 August 2017. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. Marina del Rey, Ca.: International Joint Conferences on Artificial Intelligence Organization, pp. 1074-1080. 10.24963/ijcai.2017/149

Preview

PDF - Accepted Post-Print Version Download (429kB) | Preview

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.

Item Type:	Conference or Workshop Item (Paper)
Date Type:	Publication
Status:	Published
Schools:	Computer Science & Informatics
Publisher:	International Joint Conferences on Artificial Intelligence Organization
ISBN:	978-0-9992411-0-3
Funders:	EU Horizon 2020 programme
Date of First Compliant Deposit:	4 June 2018
Last Modified:	23 Oct 2022 13:51
URI:	https://orca.cardiff.ac.uk/id/eprint/111934

Actions (repository staff only)

Edit Item