Article contents
Efficient TBox Reasoning with Value Restrictions using the
${\cal F}{{\cal L}_0}$wer Reasoner
Published online by Cambridge University Press: 15 October 2021
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 ExpTime-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 }$
.
- Type
- Original Article
- Information
- Creative Commons
- This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
- Copyright
- © The Author(s), 2021. Published by Cambridge University Press
Footnotes
This paper is under consideration in Theory and Practice of Logic Programming (TPLP).
References
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline5.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline1.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline1.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline1.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline1.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline4.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline1.png?pub-status=live)
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20220331125401901-0208:S1471068421000466:S1471068421000466_inline1.png?pub-status=live)
- 1
- Cited by