Extending ALCQIO with Trees

We study the description logic ALCQIO, which extends the standard description logic ALC with nominals, inverses and counting quantifiers. ALCQIO is a fragment of first order logic and thus cannot define trees. We consider the satisfiability problem of ALCQIO over finite structures in which k relations are interpreted as forests of directed trees with unbounded out degrees. We show that the finite satisfiability problem of ALCQIO with forests is polynomial-time reducible to finite satisfiability of ALCQIO. As a consequence, we get that finite satisfiability is NEXPTIME-complete. Description logics with transitive closure constructors or fixed points have been studied before, but we give the first decidability result of the finite satisfiability problem for a description logic that contains nominals, inverse roles, and counting quantifiers and can define trees.