TY - GEN
T1 - Efficient TBox Reasoning with Value Restrictions Using the ℱℒower Reasoner
AU - Baader, Franz
AU - Koopmann, Patrick
AU - Michel, Friedrich
AU - Turhan, Anni-Yasmin
AU - Zarriess, Benjamin
PY - 2022
Y1 - 2022
N2 - 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, that is, as hard as in the considerably more expressive logic AℒC. In the paper published in the journal Theory and Practice of Logic Programming, 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 the top and bottom concepts. We also investigate the complexity of reasoning in DLs related to the Horn-fragments of ℱℒ0 and ℱℒ⊥
AB - 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, that is, as hard as in the considerably more expressive logic AℒC. In the paper published in the journal Theory and Practice of Logic Programming, 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 the top and bottom concepts. We also investigate the complexity of reasoning in DLs related to the Horn-fragments of ℱℒ0 and ℱℒ⊥
UR - https://www.scopus.com/pages/publications/85142413956
UR - https://ceur-ws.org/Vol-3263/
M3 - Conference contribution
T3 - CEUR Workshop Proceedings
BT - DL 2022 Description Logics 2022
A2 - Arieli, O.
A2 - Homola, M.
A2 - Jung, J.C.
A2 - Mugnier, M.-L.
PB - CEUR Workshop Proceedings
T2 - 35th International Workshop on Description Logics, DL 2022
Y2 - 7 August 2022 through 10 August 2022
ER -