Efficient TBox Reasoning with Value Restrictions using the ${\mathcal{F}\mathcal{L}}_o$wer reasoner

Abstract

The inexpressive Description Logic (DL) ${\mathcal{F}\mathcal{L}}_0$, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in ${\mathcal{F}\mathcal{L}}_0$ w.r.t. general TBoxes is ExpTime-complete, i.e., as hard as in the considerably more expressive logic $\mathcal{A}\mathcal{LC}$. In this paper, we rehabilitate ${\mathcal{F}\mathcal{L}}_0$ by presenting a dedicated subsumption algorithm for ${\mathcal{F}\mathcal{L}}_0$, which is much simpler than the tableau-based algorithms employed by highly optimized DL reasoners. Our experiments show that the performance of our novel algorithm, as prototypically implemented in our ${\mathcal{F}\mathcal{L}}_o$wer reasoner, compares very well with that of the highly optimized reasoners. ${\mathcal{F}\mathcal{L}}_o$wer can also deal with ontologies written in the extension ${\mathcal{F}\mathcal{L}}_{\perp }$ of ${\mathcal{F}\mathcal{L}}_0$ with the top and the bottom concept by employing a polynomial-time reduction, shown in this paper, which eliminates top and bottom. We also investigate the complexity of reasoning in DLs related to the Horn-fragments of ${\mathcal{F}\mathcal{L}}_0$ and ${\mathcal{F}\mathcal{L}}_{\perp }$.

This paper is under consideration in Theory and Practice of Logic Programming (TPLP)