Efficient TBox Reasoning with Value Restrictions using the $\mathcal{FL}_{o}$wer reasoner

TL;DR

This paper introduces a simplified and efficient subsumption algorithm for the lightweight Description Logic $ ext{FL}_0$, demonstrating competitive performance and extending reasoning capabilities to related Horn-fragments and extensions.

Contribution

The paper presents a novel, simpler subsumption algorithm for $ ext{FL}_0$ and its extension $ ext{FL}_ot$, improving reasoning efficiency and practical applicability compared to traditional tableau-based methods.

Findings

The new algorithm performs well against highly optimized reasoners.

It can handle extensions of $ ext{FL}_0$ with polynomial-time reduction.

Complexity analysis of related Horn-fragments is provided.

Abstract

The inexpressive Description Logic (DL) $\mathcal{FL}_0$, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in $\mathcal{FL}_0$ w.r.t. general TBoxes is ExpTime-complete, i.e., as hard as in the considerably more expressive logic $\mathcal{ALC}$. In this paper, we rehabilitate $\mathcal{FL}_0$ by presenting a dedicated subsumption algorithm for $\mathcal{FL}_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{FL}_o$wer reasoner, compares very well with that of the highly optimized reasoners. $\mathcal{FL}_o$wer can also deal with ontologies written in the extension $\mathcal{FL}_{\bot}$ of $\mathcal{FL}_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{FL}_0$ and $\mathcal{FL}_{\bot}$.