Subsumption in $\mathcal{FL}_{\bot \mathit{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{FL}_{\bot\mathit{reg}}$ and the related fragments $\mathcal{FL}_{\mathit{reg}}$, $\mathcal{FL}_\bot$, and $\mathcal{FL}_0$. These formalisms support value restrictions over role names, where the subscript $\mathit{reg}$ indicates the use of regular expressions over roles. Subsumption between two concept descriptions in $\mathcal{FL}_{\bot\mathit{reg}}$ and $\mathcal{FL}_{\mathit{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{FL}_{\mathit{reg}}$ and $\mathcal{FL}_{\bot\mathit{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.