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.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:78829 |
| Date | 20 May 2022 |
| Creators | Horrocks, Ian, Sattler, Ulrike, Tobies, Stephan |
| Publisher | Aachen University of Technology |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:report, info:eu-repo/semantics/report, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:14-qucosa2-785040, qucosa:78504 |
Page generated in 0.0023 seconds