Subsumption in ${\mathcal{F}\mathcal{L}}_{\perp reg}$ with TBoxes Is in ExpTime

Abstract

Description Logics (DLs) are a family of formal languages used for representing and reasoning about structured knowledge in terms of concepts and their relationships. The expressive power of a DL depends on the constructors available for building complex concepts. In this work, we investigate subsumption in the restricted description logic ${\mathcal{F}\mathcal{L}}_{\perp reg}$ and the related fragments ${\mathcal{F}\mathcal{L}}_{reg}$, ${\mathcal{F}\mathcal{L}}_{\perp }$, and ${\mathcal{F}\mathcal{L}}_0$. These formalisms support value restrictions over role names, where the subscript $reg$ indicates the use of regular expressions over roles. Subsumption between two concept descriptions in ${\mathcal{F}\mathcal{L}}_{\perp reg}$ and ${\mathcal{F}\mathcal{L}}_{reg}$ is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. These results can be derived either from complexity bounds established for more expressive logics or from algorithms designed for harder reasoning problems. We reprove the PSpace-completeness result and provide a new proof of ExpTime-completeness for ${\mathcal{F}\mathcal{L}}_{reg}$ and ${\mathcal{F}\mathcal{L}}_{\perp reg}$ with TBoxes via a novel reduction to parity pushdown games. Our algorithm relies only on the constructs available in these logics and may therefore be implemented more easily.