Reasoning for Description logics with concrete domains and w.r.t. general TBoxes easily becomes undecidable. However, with some restriction on the concrete domain, decidability can be regained. We introduce a novel way to integrate concrete domains D into the well-known description logic ALC, we call the resulting logic ALC~P(D). We then identify sufficient conditions on D that guarantee decidability of the satisfiability problem, even in the presence of general TBoxes. In particular, we show decidability of ALC~P(D) for several domains over the integers, for which decidability was open. More generally, this result holds for all negation-closed concrete domains with the EHD-property, which stands for 'the existence of a homomorphism is definable'. Such technique has recently been used to show decidability of CTL~* with local constraints over the integers.
展开▼
