First Steps Towards Taming Description Logics with Strings

We consider the description logic ALCF(P) (D-Sigma) over the concrete domain D-Sigma = (Sigma*, <,", (=m)(m is an element of Sigma)*), where < is the strict prefix order over finite strings in Sigma*. Using an automata-based approach, we show that the concept satisfiability problem w.r.t. general TBoxes for ALCFP (D-Sigma) is ExpTime-complete for all finite alphabets Sigma. As far as we know, this is the first complexity result for an expressive description logic with a nontrivial concrete domain on strings.