# A PSpace-algorithm for deciding ALCNI_R^+-satisfiability

##### Ian HorrocksIan Horrocks,  Ulrike SattlerUlrike Sattler,  Stephan TobiesStephan Tobies
Ian Horrocks, Ulrike Sattler, Stephan Tobies
A PSpace-algorithm for deciding ALCNI_R^+-satisfiability
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-98-08, 1998. LTCS-Report
• KurzfassungAbstract
ALCI_{R^+}---ALC 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 ALCI_{R^+}-concepts. The space-efficiency of this tableau-based algorithm is due to a sophisticated guidance of the search for a solution. This algorithm will be the basis for an efficient implementation.
• Forschungsgruppe:Research Group: Automatentheorie
@techreport{ HoSatTob98,
author = {I. {Horrocks} and U. {Sattler} and S. {Tobies}},
institution = {LuFG Theoretical Computer Science, RWTH Aachen},
number = {LTCS-98-08},
title = {A PSpace-algorithm for deciding {$\mathcal{ALCNI}_{R^+}$}-satisfiability},
type = {LTCS-Report},
year = {1998},
}