Decidability of SHIQ with Complex Role Inclusion Axioms

Ian HorrocksIan Horrocks, Ulrike SattlerUlrike Sattler

Datei:HorrocksSattler-LTCS-02-06.ps.gz

Download

Ian Horrocks, Ulrike Sattler
Decidability of SHIQ with Complex Role Inclusion Axioms
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-02-06, 2002. LTCS-Report

Details
Bibtex

KurzfassungAbstract
Motivated by medical terminology applications, we investigate the decidability of an expressive and prominent DL, SHIQ, extended with role inclusion axioms of the form R o S => T (where "o" denotes composition of binary relations). It is well-known that a naive such extension leads to undecidability, and thus we restrict our attention to axioms of the form R o S => R or S o R => R, which is the most important form of axioms in the applications that motivated this extension. Surprisingly, this extension is still undecidable. However, it turns out that restricting our attention further to acyclic sets of such axioms, we regain decidability. We present a tableau-based decision procedure for this DL and report on its implementation, which behaves well in practise and provides important additional functionality in a medical terminology application.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ HorrocksSattler-LTCS-02-06,
  address = {Germany},
  author = {I. {Horrocks} and U. {Sattler}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-02-06},
  title = {Decidability of {SHIQ} with Complex Role Inclusion Axioms},
  type = {LTCS-Report},
  year = {2002},
}