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

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

Paper

Similar papers

© 2026 NYSGPT2525 LLC