• Medientyp: E-Artikel
  • Titel: Efficient TBox Reasoning with Value Restrictions using the wer Reasoner
  • Beteiligte: BAADER, FRANZ; KOOPMANN, PATRICK; MICHEL, FRIEDRICH; TURHAN, ANNI-YASMIN; ZARRIESS, BENJAMIN
  • Erschienen: Cambridge University Press (CUP), 2022
  • Erschienen in: Theory and Practice of Logic Programming
  • Sprache: Englisch
  • DOI: 10.1017/s1471068421000466
  • ISSN: 1471-0684; 1475-3081
  • Schlagwörter: Artificial Intelligence ; Computational Theory and Mathematics ; Hardware and Architecture ; Theoretical Computer Science ; Software
  • Entstehung:
  • Anmerkungen:
  • Beschreibung: <jats:title>Abstract</jats:title><jats:p>The inexpressive Description Logic (DL) <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula>, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula> w.r.t. general TBoxes is E<jats:sc>xp</jats:sc>T<jats:sc>ime</jats:sc>-complete, that is, as hard as in the considerably more expressive logic <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline2.png" /><jats:tex-math> ${\cal A}{\cal L}{\cal C}$ </jats:tex-math></jats:alternatives></jats:inline-formula>. In this paper, we rehabilitate <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula> by presenting a dedicated subsumption algorithm for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula>, 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 <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula><jats:italic>wer</jats:italic> reasoner, compares very well with that of the highly optimized reasoners. <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula><jats:italic>wer</jats:italic> can also deal with ontologies written in the extension <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline3.png" /><jats:tex-math> ${\cal F}{{\cal L}_ \bot }$ </jats:tex-math></jats:alternatives></jats:inline-formula> of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula> 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 <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline1.png" /><jats:tex-math> ${\cal F}{{\cal L}_0}$ </jats:tex-math></jats:alternatives></jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1471068421000466_inline3.png" /><jats:tex-math> ${\cal F}{{\cal L}_ \bot }$ </jats:tex-math></jats:alternatives></jats:inline-formula>.</jats:p>