Tableau Systems for SHIO and SHIQ

J. HladikJ. Hladik, J. ModelJ. Model

Download

J. Hladik, J. Model
Tableau Systems for SHIO and SHIQ
In V. Haarslev and R. Möller, eds., Proceedings of the 2004 International Workshop on Description Logics (DL 2004), 2004. CEUR

Details
Bibtex

KurzfassungAbstract
Tableau systems are a framework for tableau algorithms which tries to combine the advantages of tableau and automata algorithms, in particular efficiency in practice and worst-case complexity. In this paper, we present tableau systems for two expressive description logics, firstly the well-known SHIQ, and secondly SHIO, which has not been examined so far. The succinctness of the proofs illustrates the usefulness of the tableau system framework. As a corollary, we obtain that satisfiability of SHIO concepts is EXPTIME-complete.
Bemerkung: Note: Available from ceur-ws.org
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ HladikModel-DL-04,
  author = {J. {Hladik} and J. {Model}},
  booktitle = {Proceedings of the 2004 International Workshop on Description Logics (DL 2004)},
  editor = {V. {Haarslev} and R. {M\"oller}},
  note = {Available from \texttt{ceur-ws.org}},
  publisher = {CEUR},
  title = {Tableau Systems for {SHIO} and {SHIQ}},
  year = {2004},
}