Efficient TBox Reasoning with Value Restrictions using the 𝓕𝓛₀wer Reasoner
Publikation: Beitrag in Fachzeitschrift › Forschungsartikel › Beigetragen › Begutachtung
Beitragende
Abstract
The inexpressive Description Logic (DL) FL0, which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in FL0 w.r.t. general TBoxes is ExpTime-complete, that is, as hard as in the considerably more expressive logic ALC. In this paper, we rehabilitate FL0 by presenting a dedicated subsumption algorithm for FL0, 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 FLower reasoner, compares very well with that of the highly optimized reasoners. FLower can also deal with ontologies written in the extension FL⊥ of FL0 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 FL0 and FL⊥.
Details
Originalsprache | Englisch |
---|---|
Seiten (von - bis) | 162-192 |
Seitenumfang | 31 |
Fachzeitschrift | Theory and Practice of Logic Programming |
Jahrgang | 22 |
Ausgabenummer | 2 |
Publikationsstatus | Veröffentlicht - 15 März 2022 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 85117926349 |
---|---|
WOS | 000889154700002 |
Mendeley | 17a22ff2-cd00-374d-8011-b52517d4ab78 |
ORCID | /0000-0002-4049-221X/work/142247942 |
Schlagworte
ASJC Scopus Sachgebiete
Schlagwörter
- Description logics, Reasoning, Subsumption, description logics, reasoning, subsumption