Tableau Systems for SHIO and SHIQ

From International Center for Computational Logic

Toggle side column

Tableau Systems for SHIO and SHIQ

J. HladikJ. Hladik,  J. ModelJ. Model
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
  • 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},
}