An ExpTime Upper Bound for $\mathcal{ALC}$ with Integers (Extended Version)

TL;DR

This paper proves that reasoning in an extended version of the description logic ALC with integer domains can be done in single exponential time, matching the complexity of standard ALC, by using automata-theoretic methods.

Contribution

It introduces an extension of ALC with integer domains and shows that its reasoning complexity remains elementary, providing the first such bounds for non-dense numeric domains.

Findings

Consistency checking is in single exponential time.

Supports general TBoxes and role path comparisons.

Applies to various concrete domain extensions in description logics.

Abstract

Concrete domains, especially those that allow to compare features with numeric values, have long been recognized as a very desirable extension of description logics (DLs), and significant efforts have been invested into adding them to usual DLs while keeping the complexity of reasoning in check. For expressive DLs and in the presence of general TBoxes, for standard reasoning tasks like consistency, the most general decidability results are for the so-called $\omega$-admissible domains, which are required to be dense. Supporting non-dense domains for features that range over integers or natural numbers remained largely open, despite often being singled out as a highly desirable extension. The decidability of some extensions of $\mathcal{ALC}$ with non-dense domains has been shown, but existing results rely on powerful machinery that does not allow to infer any elementary bounds on the complexity of the problem. In this paper, we study an extension of $\mathcal{ALC}$ with a rich integer domain that allows for comparisons (between features, and between features and constants coded in unary), and prove that consistency can be solved using automata-theoretic techniques in single exponential time, and thus has no higher worst-case complexity than standard $\mathcal{ALC}$. Our upper bounds apply to some extensions of DLs with concrete domains known from the literature, support general TBoxes, and allow for comparing values along paths of ordinary (not necessarily functional) roles.