- Titel
- A PSPACE-algorithm for deciding ALCNIR+-satisfiability
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-788294
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 98-08
- Erstveröffentlichung
- 1998
- DOI
- https://doi.org/10.25368/2022.84
- Abstract (EN)
- ALCNIR+—ALCN augmented with transitive and inverse roles—is an expressive Description Logic which is especially well-suited for the representation of complex, aggregated objects. Despite its expressiveness, it has been conjectured that concept satisfiability for this logic could be decided in a comparatively efficient way. In this paper we prove the correctness of this conjecture by presenting a PSPACE algorithm for deciding satisfiability and subsumption of ALCNIR+-concepts. The space-efficiency of this tableau-based algorithm is due to a sophisticated guidance of the search for a solution. Moreover, this space-efficiency is not paid for with time-consumption; on the contrary, the guidance technique leads to very early refutation. This algorithm will be the basis for an efficient implementation.
- Freie Schlagwörter (DE)
- PSPACE-Algorithmus, Raum-Effizienz, ALCNIR+-Konzept
- Freie Schlagwörter (EN)
- PSPACE algorithm, space-efficiency, ALCNIR+-concept
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Aachen University of Technology, Aachen
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-788294
- Veröffentlichungsdatum Qucosa
- 20.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0