Lightweight description logics and branching time: a troublesome marriage

Gutierrez Basulto, Victor ORCID: https://orcid.org/0000-0002-6117-5459, Jung, Jean Christoph and Schneider, Thomas 2014. Lightweight description logics and branching time: a troublesome marriage. Presented at: Fourteenth International Conference on Principles of Knowledge Representation and Reasoning, KR 2014, Vienna, Austria, 20-24 July 2014. Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning. AAAI Publications,

Preview

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

Abstract

We study branching-time temporal description logics (BTDLs) based on the temporal logic CTL in the presence of rigid (time-invariant) roles and general TBoxes. There is evidence that, if full CTL is combined with the classical ALC in this way, reasoning becomes undecidable. In this paper, we begin by substantiating this claim, establishing undecidability for a fragment of this combination. In view of this negative result, we then investigate BTDLs that emerge from combining fragments of CTL with lightweight DLs from the EL and DL-Lite families. We show that even rather inexpressive BTDLs based on EL exhibit very high complexity. Most notably, we identify two convex fragments which are undecidable and hard for non-elementary time, respectively. For BTDLs based on DL-LiteN bool, we obtain tight complexity bounds that range from PSPACE to EXPTIME.

Item Type:	Conference or Workshop Item (Paper)
Date Type:	Publication
Status:	Published
Schools:	Computer Science & Informatics
Publisher:	AAAI Publications
Date of First Compliant Deposit:	5 June 2018
Last Modified:	23 Oct 2022 13:51
URI:	https://orca.cardiff.ac.uk/id/eprint/111950

Citation Data

Cited 12 times in Scopus. View in Scopus. Powered By Scopus® Data

Actions (repository staff only)

Edit Item