Efficient TBox Reasoning with Value Restrictions using the ${\cal F}{{\cal L}_0}$ wer Reasoner. Issue 2 (15th March 2022)

• Record Type: Journal Article
• Authors: BAADER, FRANZ; KOOPMANN, PATRICK; MICHEL, FRIEDRICH; TURHAN, ANNI-YASMIN; ZARRIESS, BENJAMIN
• Is Part Of: Theory and practice of logic programming. Volume 22:Issue 2(2022)
• Page Start: 162
• Page End: 192
• Publication Date: 2022-03-15
• Subjects: description logics -- reasoning -- subsumption; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068421000466
• Languages: English
• ISSNs: 1471-0684

Abstract

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