Efficient TBox Reasoning with Value Restrictions using the FL_0 wer Reasoner. Issue 2 (15th March 2022) - BAADER, FRANZ; KOOPMANN, PATRICK; MICHEL, FRIEDRICH; TURHAN, ANNI-YASMIN; ZARRIESS, BENJAMIN
Abstract: The inexpressive Description Logic (DL) FL_0, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in FL_0 w.r.t. general TBoxes is Exp Time -complete, that is, as hard as in the considerably more expressive logic ALC . In this paper, we rehabilitate FL_0 by presenting a dedicated subsumption algorithm for 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 FL_0 wer reasoner, compares very well with that of the highly optimized reasoners. FL_0 wer can also deal with ontologies written in the extension FL_ of 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 FL_0 and FL_ .