Efficient TBox Reasoning with Value Restrictions—Introducing the \(\mathcal {F\!L}_{o}{} \textit{wer}\) Reasoner

The Description Logic (DL) \({\mathcal {F\!L}_0}\) uses universal quantification, whereas its well-known counter-part \(\mathcal {E\!L}\) uses the existential one. While for \(\mathcal {E\!L}\) deciding subsumption in the presence of general TBoxes is tractable, this is no the case for \({\mathcal {F\!L}_0}\). We present a novel algorithm for solving the ExpTime-hard subsumption problem in \({\mathcal {F\!L}_0}\) w.r.t. general TBoxes, which is based on the computation of so-called least functional models. To build a such a model our algorithm treats TBox axioms as rules that are applied to objects of the interpretation domain. This algorithm is implemented in the \(\mathcal {F\!L}_{o}{} \textit{wer}\) reasoner, which uses a variant of the Rete pattern matching algorithm to find applicable rules. We present an evaluation of \(\mathcal {F\!L}_{o}{} \textit{wer}\) on a large set of TBoxes generated from real world ontologies. The experimental results indicate that our prototype implementation of the specialised technique for \({\mathcal {F\!L}_0}\) leads in most cases to a huge performance gain in comparison to the highly-optimised tableau reasoners.