Efficient TBox Reasoning with Value Restrictions using the ℱℒ_ower reasoner
share
The inexpressive Description Logic (DL) ℱℒ_0, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in ℱℒ_0 w.r.t. general TBoxes is ExpTime-complete, i.e., as hard as in the considerably more expressive logic 𝒜ℒ𝒞. In this paper, we rehabilitate ℱℒ_0 by presenting a dedicated subsumption algorithm for ℱℒ_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 ℱℒ_ower reasoner, compares very well with that of the highly optimized reasoners. ℱℒ_ower can also deal with ontologies written in the extension ℱℒ_ of ℱℒ_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 ℱℒ_0 and ℱℒ_.
READ FULL TEXT