Efficient TBox Reasoning with Value Restrictions—Introducing the FL_ower Reasoner

摘要

The Description Logic (DL) FL_0 uses universal quantification, whereas its well-known counter-part EL uses the existential one. While for EL deciding subsumption in the presence of general TBoxes is tractable, this is no the case for FL_0. We present a novel algorithm for solving the ExpTime-hard subsumption problem in FL_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 FL_0wer reasoner, which uses a variant of the Rete pattern matching algorithm to find applicable rules. We present an evaluation of FL_0wer on a large set of TBoxes generated from real world ontologies. The experimental results indicate that our prototype implementation of the specialised technique for FL_0 leads in most cases to a huge performance gain in comparison to the highly-optimised tableau reasoners.