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 \texttt{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},
}