A PSpace-algorithm for deciding ALCNI_R^+-satisfiability

From International Center for Computational Logic
Toggle side column

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: AutomatentheorieAutomata Theory
@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},
}