A PSpace-algorithm for deciding ALCNI_R^+-satisfiability

Ian HorrocksIan Horrocks, Ulrike SattlerUlrike Sattler, Stephan TobiesStephan Tobies

Datei:HorrocksSattlerTobies-LTCS-98-08.ps.gz

Download

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

Details
Bibtex

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},
}